public final class SimpleBlockContract extends Object implements BlockContract
Modifier and Type | Class and Description |
---|---|
private static class |
SimpleBlockContract.Combinator |
static class |
SimpleBlockContract.Creator |
private static class |
SimpleBlockContract.ReplacementMap<S extends Sorted> |
private static class |
SimpleBlockContract.TermReplacementMap |
private static class |
SimpleBlockContract.VariableReplacementMap |
BlockContract.Terms, BlockContract.Variables, BlockContract.VariablesCreator
Modifier and Type | Field and Description |
---|---|
private StatementBlock |
block |
private Map<LocationVariable,Boolean> |
hasMod |
private ImmutableList<InfFlowSpec> |
infFlowSpecs |
private Term |
instantiationSelf |
private JoinProcedure |
joinProcedure |
private List<Label> |
labels |
private IProgramMethod |
method |
private Modality |
modality |
private Map<LocationVariable,Term> |
modifiesClauses |
private Map<LocationVariable,Term> |
postconditions |
private Map<LocationVariable,Term> |
preconditions |
private boolean |
transactionApplicable |
private BlockContract.Variables |
variables |
Constructor and Description |
---|
SimpleBlockContract(StatementBlock block,
List<Label> labels,
IProgramMethod method,
Modality modality,
Map<LocationVariable,Term> preconditions,
Map<LocationVariable,Term> postconditions,
Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
JoinProcedure joinProcedure,
BlockContract.Variables variables,
boolean transactionApplicable,
Map<LocationVariable,Boolean> hasMod) |
Modifier and Type | Method and Description |
---|---|
static BlockContract |
combine(ImmutableSet<BlockContract> contracts,
Services services) |
private Map<ProgramVariable,ProgramVariable> |
createReplacementMap(BlockContract.Variables newVariables,
Services services) |
private Map<Term,Term> |
createReplacementMap(Term newHeap,
BlockContract.Terms newTerms,
Services services) |
boolean |
equals(Object obj) |
Term |
getAssignable(LocationVariable heap) |
StatementBlock |
getBlock() |
String |
getDisplayName()
Returns the displayed name.
|
Term |
getEnsures(LocationVariable heap) |
String |
getHtmlText(Services services) |
ImmutableList<InfFlowSpec> |
getInfFlowSpecs()
Returns the original information flow specification clause of the contract.
|
Term |
getInstantiationSelfTerm(TermServices services)
Returns the term internally used for self or a newly instantiated one.
|
JoinProcedure |
getJoinProcedure() |
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
List<Label> |
getLabels() |
IProgramMethod |
getMethod() |
Term |
getMod(Services services)
Returns the original modifies clause of the contract.
|
Modality |
getModality() |
Term |
getModifiesClause(LocationVariable heap,
ProgramVariable self,
Services services) |
Term |
getModifiesClause(LocationVariable heap,
Services services) |
Term |
getModifiesClause(LocationVariable heapVariable,
Term heap,
Term self,
Services services) |
String |
getName()
Returns the unique internal name of the specification element.
|
Contract.OriginalVariables |
getOrigVars() |
BlockContract.Variables |
getPlaceholderVariables() |
String |
getPlainText(Services services,
BlockContract.Terms terms) |
Term |
getPost(Services services)
Returns the original postcondition of the contract.
|
Term |
getPostcondition(LocationVariable heap,
BlockContract.Variables variables,
Services services) |
Term |
getPostcondition(LocationVariable heap,
Services services) |
Term |
getPostcondition(LocationVariable heapVariable,
Term heap,
BlockContract.Terms terms,
Services services) |
Term |
getPre(Services services)
Returns the original precondition of the contract.
|
Term |
getPrecondition(LocationVariable heap,
ProgramVariable self,
Map<LocationVariable,LocationVariable> remembranceHeaps,
Services services) |
Term |
getPrecondition(LocationVariable heap,
Services services) |
Term |
getPrecondition(LocationVariable heapVariable,
Term heap,
Term self,
Map<LocationVariable,Term> remembranceHeaps,
Services services) |
Term |
getRequires(LocationVariable heap) |
IProgramMethod |
getTarget()
Returns the method in which the block is located.
|
String |
getUniqueName() |
BlockContract.Variables |
getVariables()
Returns the original used variables like self, result etc..
|
BlockContract.Terms |
getVariablesAsTerms(Services services)
Returns the original used variables like self, result etc.
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
int |
hashCode() |
boolean |
hasInfFlowSpecs() |
boolean |
hasJoinProcedure() |
boolean |
hasMby()
Tells whether the contract contains a measured_by clause.
|
boolean |
hasModifiesClause(LocationVariable heap)
Returns
true iff the method (according to the contract) does
not modify the heap at all, i.e., iff it is "strictly pure." |
boolean |
isReadOnly(Services services) |
boolean |
isTransactionApplicable() |
BlockContract |
setBlock(StatementBlock newBlock) |
void |
setInstantiationSelf(Term selfInstantiation) |
BlockContract |
setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
String |
toString() |
BlockContract |
update(StatementBlock newBlock,
Map<LocationVariable,Term> newPreconditions,
Map<LocationVariable,Term> newPostconditions,
Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
JoinProcedure newJoinProcedure,
BlockContract.Variables newVariables) |
void |
visit(Visitor visitor) |
private final StatementBlock block
private final IProgramMethod method
private final Modality modality
private Term instantiationSelf
private final Map<LocationVariable,Term> preconditions
private final Map<LocationVariable,Term> postconditions
private final Map<LocationVariable,Term> modifiesClauses
private ImmutableList<InfFlowSpec> infFlowSpecs
private JoinProcedure joinProcedure
private final BlockContract.Variables variables
private final boolean transactionApplicable
private final Map<LocationVariable,Boolean> hasMod
public SimpleBlockContract(StatementBlock block, List<Label> labels, IProgramMethod method, Modality modality, Map<LocationVariable,Term> preconditions, Map<LocationVariable,Term> postconditions, Map<LocationVariable,Term> modifiesClauses, ImmutableList<InfFlowSpec> infFlowSpecs, JoinProcedure joinProcedure, BlockContract.Variables variables, boolean transactionApplicable, Map<LocationVariable,Boolean> hasMod)
public static BlockContract combine(ImmutableSet<BlockContract> contracts, Services services)
public StatementBlock getBlock()
getBlock
in interface BlockContract
public List<Label> getLabels()
getLabels
in interface BlockContract
public IProgramMethod getMethod()
getMethod
in interface BlockContract
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
public Modality getModality()
getModality
in interface BlockContract
public BlockContract.Variables getPlaceholderVariables()
getPlaceholderVariables
in interface BlockContract
public boolean isTransactionApplicable()
isTransactionApplicable
in interface BlockContract
public boolean isReadOnly(Services services)
isReadOnly
in interface BlockContract
public boolean hasModifiesClause(LocationVariable heap)
BlockContract
true
iff the method (according to the contract) does
not modify the heap at all, i.e., iff it is "strictly pure."hasModifiesClause
in interface BlockContract
public BlockContract.Variables getVariables()
BlockContract
getVariables
in interface BlockContract
public BlockContract.Terms getVariablesAsTerms(Services services)
BlockContract
getVariablesAsTerms
in interface BlockContract
public Term getPrecondition(LocationVariable heap, ProgramVariable self, Map<LocationVariable,LocationVariable> remembranceHeaps, Services services)
getPrecondition
in interface BlockContract
public Term getPrecondition(LocationVariable heapVariable, Term heap, Term self, Map<LocationVariable,Term> remembranceHeaps, Services services)
getPrecondition
in interface BlockContract
public Term getPrecondition(LocationVariable heap, Services services)
getPrecondition
in interface BlockContract
public Term getPostcondition(LocationVariable heap, BlockContract.Variables variables, Services services)
getPostcondition
in interface BlockContract
public Term getPostcondition(LocationVariable heapVariable, Term heap, BlockContract.Terms terms, Services services)
getPostcondition
in interface BlockContract
public Term getPostcondition(LocationVariable heap, Services services)
getPostcondition
in interface BlockContract
public Term getModifiesClause(LocationVariable heap, ProgramVariable self, Services services)
getModifiesClause
in interface BlockContract
public Term getModifiesClause(LocationVariable heapVariable, Term heap, Term self, Services services)
getModifiesClause
in interface BlockContract
public Term getModifiesClause(LocationVariable heap, Services services)
getModifiesClause
in interface BlockContract
public Term getPre(Services services)
BlockContract
getPre
in interface BlockContract
public Term getRequires(LocationVariable heap)
getRequires
in interface BlockContract
public Term getPost(Services services)
BlockContract
getPost
in interface BlockContract
public Term getEnsures(LocationVariable heap)
getEnsures
in interface BlockContract
public Term getMod(Services services)
BlockContract
getMod
in interface BlockContract
public ImmutableList<InfFlowSpec> getInfFlowSpecs()
BlockContract
getInfFlowSpecs
in interface BlockContract
public Term getAssignable(LocationVariable heap)
getAssignable
in interface BlockContract
public JoinProcedure getJoinProcedure()
getJoinProcedure
in interface BlockContract
public void visit(Visitor visitor)
visit
in interface BlockContract
public String getName()
SpecificationElement
getName
in interface SpecificationElement
public String getUniqueName()
getUniqueName
in interface BlockContract
public String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public String getHtmlText(Services services)
getHtmlText
in interface BlockContract
public String getPlainText(Services services, BlockContract.Terms terms)
getPlainText
in interface BlockContract
public VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
public BlockContract update(StatementBlock newBlock, Map<LocationVariable,Term> newPreconditions, Map<LocationVariable,Term> newPostconditions, Map<LocationVariable,Term> newModifiesClauses, ImmutableList<InfFlowSpec> newinfFlowSpecs, JoinProcedure newJoinProcedure, BlockContract.Variables newVariables)
update
in interface BlockContract
public BlockContract setBlock(StatementBlock newBlock)
setBlock
in interface BlockContract
public BlockContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
setTarget
in interface BlockContract
public Contract.OriginalVariables getOrigVars()
getOrigVars
in interface BlockContract
private Map<ProgramVariable,ProgramVariable> createReplacementMap(BlockContract.Variables newVariables, Services services)
private Map<Term,Term> createReplacementMap(Term newHeap, BlockContract.Terms newTerms, Services services)
public boolean hasMby()
BlockContract
hasMby
in interface BlockContract
public boolean hasInfFlowSpecs()
hasInfFlowSpecs
in interface BlockContract
public boolean hasJoinProcedure()
hasJoinProcedure
in interface BlockContract
public void setInstantiationSelf(Term selfInstantiation)
setInstantiationSelf
in interface BlockContract
public Term getInstantiationSelfTerm(TermServices services)
BlockContract
getInstantiationSelfTerm
in interface BlockContract
public IProgramMethod getTarget()
BlockContract
getTarget
in interface BlockContract