public class LoopInvExecutionPO extends AbstractInfFlowPO implements InfFlowCompositePO
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private ExecutionContext |
context |
private Term |
guardTerm |
private InfFlowProofSymbols |
infFlowSymbols
For saving and loading Information-Flow proofs, we need to remember the
according taclets, program variables, functions and such.
|
private Goal |
initiatingGoal |
private LoopSpecification |
loopInvariant |
private ProofObligationVars |
symbExecVars |
proofConfig
environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets, tb
PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME
Constructor and Description |
---|
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm) |
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
Modifier and Type | Method and Description |
---|---|
void |
addIFSymbol(Named n) |
void |
addIFSymbol(Term t) |
void |
addLabeledIFSymbol(Named n) |
void |
addLabeledIFSymbol(Term t) |
protected Term |
buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected java.lang.String |
buildPOName(boolean transactionFlag)
Returns the name of the
Proof based on the given transaction flag. |
void |
fillSaveProperties(java.util.Properties properties)
This method is called by a
ProofSaver to store the proof
specific settings in the given Properties . |
protected Term |
generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected KeYJavaType |
getCalleeKeYJavaType()
Returns the
KeYJavaType which contains AbstractOperationPO.getProgramMethod() . |
AbstractInfFlowPO |
getChildPO() |
ExecutionContext |
getExecutionContext() |
protected Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
Term |
getGuard() |
InfFlowProofSymbols |
getIFSymbols() |
Goal |
getInitiatingGoal() |
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.
|
LoopSpecification |
getLoopInvariant() |
protected Term |
getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected Term |
getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected IProgramMethod |
getProgramMethod()
Returns the
IProgramMethod to call. |
protected Modality |
getTerminationMarker()
Returns the
Modality to use as termination marker. |
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
protected boolean |
isTransactionApplicable()
Checks if transactions are applicable.
|
private boolean |
preAndPostExpressionsEqual() |
void |
readProblem() |
void |
unionLabeledIFSymbols(InfFlowProofSymbols symbols) |
createProof, createProofObject
addAdditionalUninterpretedPredicateIfRequired, addUninterpretedPredicateIfRequired, buildFreePre, buildJavaBlock, buildProgramTerm, buildUpdate, createUninterpretedPredicate, ensureUninterpretedPredicateExists, generateParamsOK, generateParamsOK2, getAdditionalUninterpretedPredicates, getAdditionalUninterpretedPredicates, getBaseHeap, getCreatedInitConfigForSingleProof, getInitialTaclets, getSavedHeap, getUninterpretedPredicate, getUninterpretedPredicate, getUninterpretedPredicateName, isAddSymbolicExecutionLabel, isAddSymbolicExecutionLabel, isAddUninterpretedPredicate, isAddUninterpretedPredicate, isCopyOfMethodArgumentsUsed, isMakeNamesUnique, modifyPostTerm, newAdditionalUninterpretedPredicate, postInit
assignPOTerms, collectClassAxioms, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, getContainerType, getName, getPO, name, register, register, register, selectClassAxioms
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getContainerType, getPO, name
private final LoopSpecification loopInvariant
private final ProofObligationVars symbExecVars
private final Term guardTerm
private final Goal initiatingGoal
private final ExecutionContext context
private InfFlowProofSymbols infFlowSymbols
public LoopInvExecutionPO(InitConfig initConfig, LoopSpecification loopInv, ProofObligationVars symbExecVars, Goal initiatingGoal, ExecutionContext context, Term guardTerm, Services services)
public LoopInvExecutionPO(InitConfig initConfig, LoopSpecification loopInv, ProofObligationVars symbExecVars, Goal initiatingGoal, ExecutionContext context, Term guardTerm)
private boolean preAndPostExpressionsEqual()
public void readProblem() throws ProofInputException
AbstractOperationPO
readProblem
in interface ProofOblInput
readProblem
in class AbstractOperationPO
ProofInputException
public boolean implies(ProofOblInput po)
ProofOblInput
implies
in interface ProofOblInput
implies
in class AbstractPO
public LoopSpecification getLoopInvariant()
public Goal getInitiatingGoal()
public ExecutionContext getExecutionContext()
public Term getGuard()
protected IProgramMethod getProgramMethod()
AbstractOperationPO
IProgramMethod
to call.getProgramMethod
in class AbstractOperationPO
IProgramMethod
to call.protected boolean isTransactionApplicable()
AbstractOperationPO
isTransactionApplicable
in class AbstractOperationPO
protected KeYJavaType getCalleeKeYJavaType()
AbstractOperationPO
KeYJavaType
which contains AbstractOperationPO.getProgramMethod()
.getCalleeKeYJavaType
in class AbstractOperationPO
KeYJavaType
which contains AbstractOperationPO.getProgramMethod()
.protected Modality getTerminationMarker()
AbstractOperationPO
Modality
to use as termination marker.getTerminationMarker
in class AbstractOperationPO
Modality
to use as termination marker.protected java.lang.String buildPOName(boolean transactionFlag)
AbstractOperationPO
Proof
based on the given transaction flag.buildPOName
in class AbstractOperationPO
transactionFlag
- The transaction flag.public void fillSaveProperties(java.util.Properties properties) throws java.io.IOException
ProofSaver
to store the proof
specific settings in the given Properties
. The stored settings
have to contain all information required to instantiate the proof
obligation again and this instance should create the same Sequent
(if code and specifications are unchanged).fillSaveProperties
in interface IPersistablePO
fillSaveProperties
in class AbstractOperationPO
properties
- The Properties
to fill with the proof obligation specific settings.java.io.IOException
- Occurred Exception.public InfFlowProofSymbols getIFSymbols()
getIFSymbols
in interface InfFlowPO
public void addIFSymbol(Term t)
addIFSymbol
in interface InfFlowPO
public void addIFSymbol(Named n)
addIFSymbol
in interface InfFlowPO
public void addLabeledIFSymbol(Term t)
addLabeledIFSymbol
in interface InfFlowPO
public void addLabeledIFSymbol(Named n)
addLabeledIFSymbol
in interface InfFlowPO
public void unionLabeledIFSymbols(InfFlowProofSymbols symbols)
unionLabeledIFSymbols
in interface InfFlowPO
protected Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
getGlobalDefs
in class AbstractOperationPO
public AbstractInfFlowPO getChildPO()
getChildPO
in interface InfFlowCompositePO
public IFProofObligationVars getLeafIFVars()
InfFlowPO
getLeafIFVars
in interface InfFlowPO
@Deprecated protected ImmutableList<StatementBlock> buildOperationBlocks(ImmutableList<LocationVariable> formalParVars, ProgramVariable selfVar, ProgramVariable resultVar, Services services)
AbstractOperationPO
buildOperationBlocks
in class AbstractOperationPO
formalParVars
- Arguments from formal parameters for method call.selfVar
- The self variable.resultVar
- The result variable.services
- services instance@Deprecated protected Term generateMbyAtPreDef(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
generateMbyAtPreDef
in class AbstractOperationPO
@Deprecated protected Term getPre(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services)
AbstractOperationPO
getPre
in class AbstractOperationPO
modHeaps
- The heaps.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.atPreVars
- Mapping of LocationVariable
to the
LocationVariable
which contains the initial value.services
- The Services
to use.Term
representing the precondition.@Deprecated protected Term getPost(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable exceptionVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services)
AbstractOperationPO
getPost
in class AbstractOperationPO
modHeaps
- The heaps.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.resultVar
- The result variable.exceptionVar
- The exception variable.atPreVars
- Mapping of LocationVariable
to the
LocationVariable
which contains the initial value.services
- The Services
to use.Term
representing the postcondition.@Deprecated protected Term buildFrameClause(java.util.List<LocationVariable> modHeaps, java.util.Map<Term,Term> heapToAtPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
AbstractOperationPO
buildFrameClause
in class AbstractOperationPO
modHeaps
- The heaps.heapToAtPre
- The previous heap before execution.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.services
- services instanceTerm
representing the frame clause.