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 LoopInvariant |
loopInvariant |
private ProofObligationVars |
symbExecVars |
proofConfig, tb
environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets
PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME
Constructor and Description |
---|
LoopInvExecutionPO(InitConfig initConfig,
LoopInvariant loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm) |
LoopInvExecutionPO(InitConfig initConfig,
LoopInvariant 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.
|
createProof, createProofObject
addAdditionalUninterpretedPredicateIfRequired, addUninterpretedPredicateIfRequired, buildFreePre, buildJavaBlock, buildProgramTerm, buildUpdate, createUninterpretedPredicate, ensureUninterpretedPredicateExists, generateParamsOK, generateParamsOK2, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, getAdditionalUninterpretedPredicates, getAdditionalUninterpretedPredicates, getBaseHeap, getCreatedInitConfigForSingleProof, getInitialTaclets, getSavedHeap, getUninterpretedPredicate, getUninterpretedPredicate, getUninterpretedPredicateName, isAddSymbolicExecutionLabel, isAddSymbolicExecutionLabel, isAddUninterpretedPredicate, isAddUninterpretedPredicate, isCopyOfMethodArgumentsUsed, isMakeNamesUnique, modifyPostTerm, newAdditionalUninterpretedPredicate, postInit
assignPOTerms, collectClassAxioms, getContainerType, getName, getPO, name, register, register, register, selectClassAxioms
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getContainerType, getPO, name
private final LoopInvariant loopInvariant
private final ProofObligationVars symbExecVars
private final Term guardTerm
private final Goal initiatingGoal
private final ExecutionContext context
private InfFlowProofSymbols infFlowSymbols
public LoopInvExecutionPO(InitConfig initConfig, LoopInvariant loopInv, ProofObligationVars symbExecVars, Goal initiatingGoal, ExecutionContext context, Term guardTerm, Services services)
public LoopInvExecutionPO(InitConfig initConfig, LoopInvariant 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 LoopInvariant 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
protected String buildPOName(boolean transactionFlag)
AbstractOperationPO
Proof
based on the given transaction flag.buildPOName
in class AbstractOperationPO
transactionFlag
- The transaction flag.public void fillSaveProperties(Properties properties) throws 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.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 getLeaveIFVars()
getLeaveIFVars
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
- TODO@Deprecated protected Term generateMbyAtPreDef(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
generateMbyAtPreDef
in class AbstractOperationPO
@Deprecated protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, 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(List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable exceptionVar, 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(List<LocationVariable> modHeaps, 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
- TODOTerm
representing the frame clause.