public interface InfFlowPO extends ProofOblInput
Modifier and Type | Method and Description |
---|---|
void |
addIFSymbol(Named n) |
void |
addIFSymbol(Term t) |
void |
addLabeledIFSymbol(Named n) |
void |
addLabeledIFSymbol(Term t) |
InfFlowProofSymbols |
getIFSymbols() |
IFProofObligationVars |
getLeafIFVars()
Get the information flow proof obligation variables (set of four sets of
proof obligation variables necessary for information flow proofs) for
the "leaf" (i.e., child of child of ..) information flow proof
obligation.
|
void |
unionLabeledIFSymbols(InfFlowProofSymbols symbols) |
getContainerType, getPO, implies, name, readProblem
IFProofObligationVars getLeafIFVars()
InfFlowProofSymbols getIFSymbols()
void addIFSymbol(Term t)
void addIFSymbol(Named n)
void addLabeledIFSymbol(Term t)
void addLabeledIFSymbol(Named n)
void unionLabeledIFSymbols(InfFlowProofSymbols symbols)