public class ProgramMethodSubsetPO extends ProgramMethodPO
This proof obligation executes selected statements of the body
of a given IProgramMethod
. The statements are selected by its
source location. All statements which ends in the given source range
]startPosition
, endPosition
] are executed.
To select statements by its end position is required, because KeY's recorder includes also leading space and leading comments into a statements position. Another drawback is that the end position of the previous statement is exactly the start position of the following statement.
Imagine the following snippet:
To execute only the last two statements a user would select intuitively
the source range 5/0 to 6/16 (the text without leading white space) which
matches exactly the used selection definition.
int x = 1; // from 3/59 to 4/16
int y = 2; // from 4/16 to 5/16
int z = 3; // from 5/16 to 6/16
The generated Sequent
has the following form:
==>
<generalAssumptions> &
<preconditions>
->
<updatesToStoreInitialValues>
<modalityStart>
exc=null;try {<methodFrame><selectedStatements>}catch(java.lang.Exception e) {exc = e}
<modalityEnd>
(exc = null & <postconditions > & <optionalUninterpretedPredicate>)
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private Position |
endPosition
The end position.
|
private Position |
startPosition
The start position.
|
private UndeclaredProgramVariableCollector |
undeclaredVariableCollector
Contains all undeclared variables used in the method part to execute.
|
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 |
---|
ProgramMethodSubsetPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
Position startPosition,
Position endPosition)
Constructor.
|
ProgramMethodSubsetPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
Position startPosition,
Position endPosition,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected Term |
buildFreePre(ProgramVariable selfVar,
KeYJavaType selfKJT,
ImmutableList<ProgramVariable> paramVars,
java.util.List<LocationVariable> heaps,
Services proofServices)
Builds the "general assumption".
|
protected ImmutableList<StatementBlock> |
buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
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
|
protected void |
collectStatementsToExecute(java.util.List<Statement> toFill,
StatementContainer container)
Collects recursive the
Statement s which are in the given source range
defined by startPosition and endPosition . |
protected static ImmutableList<ProgramVariable> |
convert(java.util.Collection<LocationVariable> c)
Converts the given
Collection into an ImmutableList . |
protected boolean |
endsWithReturn(Statement[] statements)
Checks if the last statement is a
Return statement. |
protected Term |
ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable exceptionVar,
java.lang.String name,
Services proofServices)
|
boolean |
equals(java.lang.Object obj) |
void |
fillSaveProperties(java.util.Properties properties)
This method is called by a
ProofSaver to store the proof
specific settings in the given Properties . |
Position |
getEndPosition()
Returns the end position.
|
protected static Position |
getEndPosition(java.util.Properties properties)
Extracts the end position from the given
Properties . |
protected Term |
getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
Position |
getStartPosition()
Returns the start position.
|
protected static Position |
getStartPosition(java.util.Properties properties)
Extracts the start position from the given
Properties . |
int |
hashCode() |
static IPersistablePO.LoadedPOContainer |
loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
buildFrameClause, buildPOName, generateMbyAtPreDef, getCalleeKeYJavaType, getContainerType, getGlobalDefs, getPost, getPrecondition, getPrecondition, getProgramMethod, getProgramMethod, getProgramMethodSignature, getTerminationMarker, isCopyOfMethodArgumentsUsed, isMakeNamesUnique, isTransactionApplicable
addAdditionalUninterpretedPredicateIfRequired, addUninterpretedPredicateIfRequired, buildJavaBlock, buildProgramTerm, buildUpdate, createUninterpretedPredicate, generateParamsOK, generateParamsOK2, getAdditionalUninterpretedPredicates, getAdditionalUninterpretedPredicates, getBaseHeap, getCreatedInitConfigForSingleProof, getInitialTaclets, getSavedHeap, getUninterpretedPredicate, getUninterpretedPredicate, getUninterpretedPredicateName, isAddSymbolicExecutionLabel, isAddSymbolicExecutionLabel, isAddUninterpretedPredicate, isAddUninterpretedPredicate, modifyPostTerm, newAdditionalUninterpretedPredicate, postInit, readProblem
assignPOTerms, collectClassAxioms, createProof, createProofObject, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, getName, getPO, implies, name, register, register, register, selectClassAxioms
private UndeclaredProgramVariableCollector undeclaredVariableCollector
private Position startPosition
private Position endPosition
public ProgramMethodSubsetPO(InitConfig initConfig, java.lang.String name, IProgramMethod pm, java.lang.String precondition, Position startPosition, Position endPosition)
initConfig
- The InitConfig
to use.name
- The name to use.pm
- The IProgramMethod
to execute code parts from.precondition
- An optional precondition to use.startPosition
- The start position.endPosition
- The end position.public ProgramMethodSubsetPO(InitConfig initConfig, java.lang.String name, IProgramMethod pm, java.lang.String precondition, Position startPosition, Position endPosition, boolean addUninterpretedPredicate, boolean addSymbolicExecutionLabel)
initConfig
- The InitConfig
to use.name
- The name to use.pm
- The IProgramMethod
to execute code parts from.precondition
- An optional precondition to use.startPosition
- The start position.endPosition
- The end position.addUninterpretedPredicate
- true
postcondition contains uninterpreted predicate, false
uninterpreted predicate is not contained in postcondition.addSymbolicExecutionLabel
- true
to add the SymbolicExecutionTermLabel
to the modality, false
to not label the modality.protected ImmutableList<StatementBlock> buildOperationBlocks(ImmutableList<LocationVariable> formalParVars, ProgramVariable selfVar, ProgramVariable resultVar, Services services)
buildOperationBlocks
in class ProgramMethodPO
formalParVars
- Arguments from formal parameters for method call.selfVar
- The self variable.resultVar
- The result variable.services
- services instanceprotected void collectStatementsToExecute(java.util.List<Statement> toFill, StatementContainer container)
Statement
s which are in the given source range
defined by startPosition
and endPosition
.toFill
- The result List
to fill.container
- The StatementContainer
to seach in.protected boolean endsWithReturn(Statement[] statements)
Return
statement.statements
- The statements to check.true
last statement is Return
, false
statements are empty or last statement is something else.protected Term getPre(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services)
getPre
in class ProgramMethodPO
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.protected Term buildFreePre(ProgramVariable selfVar, KeYJavaType selfKJT, ImmutableList<ProgramVariable> paramVars, java.util.List<LocationVariable> heaps, Services proofServices)
buildFreePre
in class AbstractOperationPO
selfVar
- The self variable.selfKJT
- The KeYJavaType
of the self variable.paramVars
- The parameters ProgramVariable
s.heaps
- The heaps.proofServices
- The services instance.Term
containing the general assumptions.protected Term ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars, ImmutableList<LocationVariable> formalParamVars, ProgramVariable exceptionVar, java.lang.String name, Services proofServices)
ensureUninterpretedPredicateExists
in class AbstractOperationPO
paramVars
- The parameters ProgramVariable
s.formalParamVars
- The formal parameters LocationVariable
s.exceptionVar
- The exception variable.name
- The name of the uninterpreted predicate.proofServices
- services instance.protected static ImmutableList<ProgramVariable> convert(java.util.Collection<LocationVariable> c)
Collection
into an ImmutableList
.c
- The Collection
to convert.ImmutableList
.public int hashCode()
hashCode
in class ProgramMethodPO
public boolean equals(java.lang.Object obj)
equals
in class ProgramMethodPO
public Position getStartPosition()
public Position getEndPosition()
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 ProgramMethodPO
properties
- The Properties
to fill with the proof obligation specific settings.java.io.IOException
- Occurred Exception.public static IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig, java.util.Properties properties) throws java.io.IOException
initConfig
- The already load InitConfig
.properties
- The settings of the proof obligation to instantiate.java.io.IOException
- Occurred Exception.protected static Position getStartPosition(java.util.Properties properties) throws java.io.IOException
Properties
.properties
- The proof obligation settings to read from.Position
.java.io.IOException
- Occurred Exception if it was not possible to read the start position.protected static Position getEndPosition(java.util.Properties properties) throws java.io.IOException
Properties
.properties
- The proof obligation settings to read from.Position
.java.io.IOException
- Occurred Exception if it was not possible to read the end position.