de.uka.ilkd.key.informationflow.po

Class LoopInvExecutionPO

java.lang.Object

de.uka.ilkd.key.proof.init.AbstractPO

de.uka.ilkd.key.proof.init.AbstractOperationPO

de.uka.ilkd.key.informationflow.po.AbstractInfFlowPO

de.uka.ilkd.key.informationflow.po.LoopInvExecutionPO

All Implemented Interfaces:

InfFlowCompositePO, InfFlowPO, IPersistablePO, ProofOblInput

public class LoopInvExecutionPO
extends AbstractInfFlowPO
implements InfFlowCompositePO

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.proof.init.IPersistablePO

IPersistablePO.LoadedPOContainer

Field Summary

Fields

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

Fields inherited from class de.uka.ilkd.key.proof.init.AbstractOperationPO

proofConfig

Fields inherited from class de.uka.ilkd.key.proof.init.AbstractPO

environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets, tb

Fields inherited from interface de.uka.ilkd.key.proof.init.IPersistablePO

PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME

Constructor Summary

Constructors

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.

Method Summary

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)

Methods inherited from class de.uka.ilkd.key.informationflow.po.AbstractInfFlowPO

createProof, createProofObject

Methods inherited from class de.uka.ilkd.key.proof.init.AbstractOperationPO

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

Methods inherited from class de.uka.ilkd.key.proof.init.AbstractPO

assignPOTerms, collectClassAxioms, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, getContainerType, getName, getPO, name, register, register, register, selectClassAxioms

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.proof.init.ProofOblInput

getContainerType, getPO, name

Field Detail

loopInvariant

private final LoopSpecification loopInvariant

symbExecVars

private final ProofObligationVars symbExecVars

guardTerm

private final Term guardTerm

initiatingGoal

private final Goal initiatingGoal

context

private final ExecutionContext context

infFlowSymbols

private InfFlowProofSymbols infFlowSymbols

For saving and loading Information-Flow proofs, we need to remember the according taclets, program variables, functions and such.

Constructor Detail

LoopInvExecutionPO

public 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.

LoopInvExecutionPO

public LoopInvExecutionPO(InitConfig initConfig,
                          LoopSpecification loopInv,
                          ProofObligationVars symbExecVars,
                          Goal initiatingGoal,
                          ExecutionContext context,
                          Term guardTerm)

Method Detail

preAndPostExpressionsEqual

private boolean preAndPostExpressionsEqual()

readProblem

public void readProblem()
                 throws ProofInputException

Description copied from class: AbstractOperationPO

Specified by:

readProblem in interface ProofOblInput

Overrides:

readProblem in class AbstractOperationPO

Throws:

ProofInputException

implies

public boolean implies(ProofOblInput po)

Description copied from interface: ProofOblInput

If true, then this PO implies the passed one.

Specified by:

implies in interface ProofOblInput

Overrides:

implies in class AbstractPO

getLoopInvariant

public LoopSpecification getLoopInvariant()

getInitiatingGoal

public Goal getInitiatingGoal()

getExecutionContext

public ExecutionContext getExecutionContext()

getGuard

public Term getGuard()

getProgramMethod

protected IProgramMethod getProgramMethod()

Description copied from class: AbstractOperationPO

Returns the IProgramMethod to call.

Specified by:

getProgramMethod in class AbstractOperationPO

Returns:

The IProgramMethod to call.

isTransactionApplicable

protected boolean isTransactionApplicable()

Description copied from class: AbstractOperationPO

Checks if transactions are applicable.

Specified by:

isTransactionApplicable in class AbstractOperationPO

Returns:

Transactions are applicable?

getCalleeKeYJavaType

protected KeYJavaType getCalleeKeYJavaType()

Description copied from class: AbstractOperationPO

Returns the KeYJavaType which contains AbstractOperationPO.getProgramMethod().

Specified by:

getCalleeKeYJavaType in class AbstractOperationPO

Returns:

The KeYJavaType which contains AbstractOperationPO.getProgramMethod().

getTerminationMarker

protected Modality getTerminationMarker()

Description copied from class: AbstractOperationPO

Returns the Modality to use as termination marker.

Specified by:

getTerminationMarker in class AbstractOperationPO

Returns:

The Modality to use as termination marker.

buildPOName

protected java.lang.String buildPOName(boolean transactionFlag)

Description copied from class: AbstractOperationPO

Returns the name of the Proof based on the given transaction flag.

Specified by:

buildPOName in class AbstractOperationPO

Parameters:

transactionFlag - The transaction flag.

Returns:

The proof name to use.

fillSaveProperties

public void fillSaveProperties(java.util.Properties properties)
                        throws java.io.IOException

This method is called by a 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).

Specified by:

fillSaveProperties in interface IPersistablePO

Overrides:

fillSaveProperties in class AbstractOperationPO

Parameters:

properties - The Properties to fill with the proof obligation specific settings.

Throws:

java.io.IOException - Occurred Exception.

getIFSymbols

public InfFlowProofSymbols getIFSymbols()

Specified by:

getIFSymbols in interface InfFlowPO

addIFSymbol

public void addIFSymbol(Term t)

Specified by:

addIFSymbol in interface InfFlowPO

addIFSymbol

public void addIFSymbol(Named n)

Specified by:

addIFSymbol in interface InfFlowPO

addLabeledIFSymbol

public void addLabeledIFSymbol(Term t)

Specified by:

addLabeledIFSymbol in interface InfFlowPO

addLabeledIFSymbol

public void addLabeledIFSymbol(Named n)

Specified by:

addLabeledIFSymbol in interface InfFlowPO

unionLabeledIFSymbols

public void unionLabeledIFSymbols(InfFlowProofSymbols symbols)

Specified by:

unionLabeledIFSymbols in interface InfFlowPO

getGlobalDefs

protected Term getGlobalDefs(LocationVariable heap,
                             Term heapTerm,
                             Term selfTerm,
                             ImmutableList<Term> paramTerms,
                             Services services)

Specified by:

getGlobalDefs in class AbstractOperationPO

getChildPO

public AbstractInfFlowPO getChildPO()

Specified by:

getChildPO in interface InfFlowCompositePO

getLeafIFVars

public IFProofObligationVars getLeafIFVars()

Description copied from interface: InfFlowPO

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.

Specified by:

getLeafIFVars in interface InfFlowPO

Returns:

the information flow proof obligation variables.

buildOperationBlocks

@Deprecated
protected ImmutableList<StatementBlock> buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
                                                                         ProgramVariable selfVar,
                                                                         ProgramVariable resultVar,
                                                                         Services services)

Deprecated.

Description copied from class: AbstractOperationPO

Builds the code to execute in different statement blocks. 1. code to execute before the try block 2. code to execute in the try block 3. code to execute in the catch block 4. code to execute in the finally block

Specified by:

buildOperationBlocks in class AbstractOperationPO

Parameters:

formalParVars - Arguments from formal parameters for method call.

selfVar - The self variable.

resultVar - The result variable.

services - services instance

Returns:

operation blocks as statement blocks

generateMbyAtPreDef

@Deprecated
protected Term generateMbyAtPreDef(ProgramVariable selfVar,
                                               ImmutableList<ProgramVariable> paramVars,
                                               Services services)

Deprecated.

Specified by:

generateMbyAtPreDef in class AbstractOperationPO

getPre

@Deprecated
protected Term getPre(java.util.List<LocationVariable> modHeaps,
                                  ProgramVariable selfVar,
                                  ImmutableList<ProgramVariable> paramVars,
                                  java.util.Map<LocationVariable,LocationVariable> atPreVars,
                                  Services services)

Deprecated.

Description copied from class: AbstractOperationPO

Creates the precondition.

Specified by:

getPre in class AbstractOperationPO

Parameters:

modHeaps - The heaps.

selfVar - The self variable.

paramVars - The parameters ProgramVariables.

atPreVars - Mapping of LocationVariable to the LocationVariable which contains the initial value.

services - The Services to use.

Returns:

The Term representing the precondition.

getPost

@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)

Deprecated.

Description copied from class: AbstractOperationPO

Creates the postcondition.

Specified by:

getPost in class AbstractOperationPO

Parameters:

modHeaps - The heaps.

selfVar - The self variable.

paramVars - The parameters ProgramVariables.

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.

Returns:

The Term representing the postcondition.

buildFrameClause

@Deprecated
protected Term buildFrameClause(java.util.List<LocationVariable> modHeaps,
                                            java.util.Map<Term,Term> heapToAtPre,
                                            ProgramVariable selfVar,
                                            ImmutableList<ProgramVariable> paramVars,
                                            Services services)

Deprecated.

Description copied from class: AbstractOperationPO

Builds the frame clause including the modifies clause.

Specified by:

buildFrameClause in class AbstractOperationPO

Parameters:

modHeaps - The heaps.

heapToAtPre - The previous heap before execution.

selfVar - The self variable.

paramVars - The parameters ProgramVariables.

services - services instance

Returns:

The created Term representing the frame clause.