public final class InformationFlowContractImpl extends Object implements InformationFlowContract
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
private String |
baseName |
private KeYJavaType |
forClass |
(package private) boolean |
hasRealModifiesClause
If a method is strictly pure, it has no modifies clause which could
anonymised.
|
private int |
id |
private Modality |
modality |
private String |
name |
private Term |
origAtPre |
private Term |
origDep |
private Term |
origExc |
private ImmutableList<InfFlowSpec> |
origInfFlowSpecs |
private Term |
origMby |
private Term |
origMod |
private ImmutableList<Term> |
origParams |
private Term |
origPre |
private Term |
origResult |
private Term |
origSelf |
private IProgramMethod |
pm |
private KeYJavaType |
specifiedIn |
private boolean |
toBeSaved |
INVALID_ID
Modifier | Constructor and Description |
---|---|
|
InformationFlowContractImpl(String baseName,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
protected |
InformationFlowContractImpl(String baseName,
String name,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved,
int id) |
Modifier and Type | Method and Description |
---|---|
ContractPO |
createProofObl(InitConfig initConfig)
Returns a proof obligation to the passed contract and initConfig.
|
ProofOblInput |
createProofObl(InitConfig initConfig,
Contract contract)
Returns a proof obligation to the passed contract and initConfig.
|
ProofOblInput |
createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel)
Returns a proof obligation to the passed contract and initConfig.
|
boolean |
equals(Contract c) |
Term |
getAccessible(ProgramVariable heap) |
Term |
getAssignable(LocationVariable heap) |
Term |
getAtPre() |
String |
getBaseName() |
Term |
getDep()
Returns the dependency set of the contract.
|
Term |
getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the dependency set of the contract.
|
Term |
getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Map<LocationVariable,Term> atPres,
Services services)
Returns the dependency set of the contract.
|
String |
getDisplayName()
Returns the displayed name.
|
Term |
getExc()
Get the exception-variable which is used in this contract.
|
Term |
getGlobalDefs() |
Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
String |
getHTMLBody(Services services) |
private String |
getHTMLFor(ImmutableList<InfFlowSpec> originalInfFlowSpecs,
String htmlName,
Services services) |
private String |
getHTMLFor(Iterable<Term> originalTerms,
Services services) |
protected String |
getHTMLFor(Term originalTerm,
String htmlName,
Services services) |
private String |
getHTMLSignature() |
private StringBuffer |
getHTMLSignatureBody() |
String |
getHTMLText(Services services)
Returns the contract in pretty HTML format.
|
ImmutableList<InfFlowSpec> |
getInfFlowSpecs()
Returns the set of views.
|
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
Term |
getMby()
Returns the original measured_by clause of the contract.
|
Term |
getMby(Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
Term |
getMod()
Returns the original modifies clause of the contract.
|
Modality |
getModality()
Returns the modality of the contract.
|
String |
getName()
Returns the unique internal name of the specification element.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original ProgramVariables to replace them easier.
|
ImmutableList<Term> |
getParams()
Get the parameter-variables which is used in this contract.
|
String |
getPlainText(Services services)
Returns the contract in pretty plain text format.
|
String |
getPODisplayName()
For generating contract name of SymbolicExecutionPO
|
Term |
getPre()
Returns the original precondition of the contract.
|
Term |
getPre(List<LocationVariable> heapContext,
Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
getPre(List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
ProofOblInput |
getProofObl(Services services)
Lookup the proof obligation belonging to the contract in the
specification repository.
|
Term |
getRequires(LocationVariable heap) |
Term |
getResult()
Get the result-variable which is used in this contract.
|
Term |
getSelf()
Get the self-variable which is used in this contract.
|
KeYJavaType |
getSpecifiedIn() |
IProgramMethod |
getTarget()
Returns the contracted function symbol.
|
String |
getTypeName()
Returns technical name for the contract type.
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
boolean |
hasInfFlowSpec() |
boolean |
hasMby()
Tells whether the contract contains a measured_by clause.
|
boolean |
hasModifiesClause()
Returns
true iff the method (according to the contract) does
not modify the heap at all, i.e., iff it is "strictly pure." |
boolean |
hasSelfVar()
Checks if a self variable is originally provided.
|
int |
id()
Returns the id number of the contract.
|
boolean |
isReadOnlyContract() |
String |
proofToString(Services services)
Returns a parseable String representation of the contract.
|
InformationFlowContract |
setID(int newId)
Return a new contract which equals this contract except that the id is
set to the new id.
|
InformationFlowContract |
setModality(Modality modality) |
InformationFlowContract |
setModifies(Term modifies) |
InformationFlowContract |
setName(String name) |
InformationFlowContract |
setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Return a new contract which equals this contract except that the
the KeYJavaType and ObserverFunction are set to the new values.
|
boolean |
toBeSaved()
Tells whether, on saving a proof where this contract is available, the
contract should be saved too.
|
String |
toString() |
boolean |
transactionApplicableContract() |
private final int id
private final KeYJavaType forClass
private final IProgramMethod pm
private final KeYJavaType specifiedIn
private final String baseName
private final String name
private final Term origPre
private final Term origMby
private final Term origMod
private final Modality modality
private final Term origSelf
private final ImmutableList<Term> origParams
private final Term origResult
private final Term origExc
private final Term origAtPre
private final boolean toBeSaved
private final Term origDep
private final ImmutableList<InfFlowSpec> origInfFlowSpecs
final boolean hasRealModifiesClause
hasModifiesClause()
protected InformationFlowContractImpl(String baseName, String name, KeYJavaType forClass, IProgramMethod pm, KeYJavaType specifiedIn, Modality modality, Term pre, Term mby, Term mod, boolean hasRealMod, Term self, ImmutableList<Term> params, Term result, Term exc, Term heapAtPre, Term dep, ImmutableList<InfFlowSpec> infFlowSpecs, boolean toBeSaved, int id)
public InformationFlowContractImpl(String baseName, KeYJavaType forClass, IProgramMethod pm, KeYJavaType specifiedIn, Modality modality, Term pre, Term mby, Term mod, boolean hasRealMod, Term self, ImmutableList<Term> params, Term result, Term exc, Term heapAtPre, Term dep, ImmutableList<InfFlowSpec> infFlowSpecs, boolean toBeSaved)
public String getName()
SpecificationElement
getName
in interface SpecificationElement
public int id()
Contract
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
public IProgramMethod getTarget()
Contract
getTarget
in interface Contract
getTarget
in interface InformationFlowContract
public boolean hasMby()
Contract
public String getBaseName()
getBaseName
in interface InformationFlowContract
public Term getPre()
InformationFlowContract
getPre
in interface InformationFlowContract
public Term getMod()
InformationFlowContract
getMod
in interface InformationFlowContract
public Term getMby()
InformationFlowContract
getMby
in interface Contract
getMby
in interface InformationFlowContract
public Modality getModality()
InformationFlowContract
getModality
in interface InformationFlowContract
public Term getSelf()
InformationFlowContract
getSelf
in interface InformationFlowContract
public ImmutableList<Term> getParams()
InformationFlowContract
getParams
in interface InformationFlowContract
public Term getResult()
InformationFlowContract
getResult
in interface InformationFlowContract
public Term getExc()
InformationFlowContract
getExc
in interface InformationFlowContract
public Term getAtPre()
getAtPre
in interface InformationFlowContract
public boolean isReadOnlyContract()
isReadOnlyContract
in interface InformationFlowContract
public String getTypeName()
Contract
getTypeName
in interface Contract
public boolean hasModifiesClause()
InformationFlowContract
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 InformationFlowContract
public boolean hasInfFlowSpec()
hasInfFlowSpec
in interface InformationFlowContract
public String getHTMLText(Services services)
Contract
getHTMLText
in interface Contract
private String getHTMLSignature()
private StringBuffer getHTMLSignatureBody()
private String getHTMLFor(ImmutableList<InfFlowSpec> originalInfFlowSpecs, String htmlName, Services services)
public final ContractPO createProofObl(InitConfig initConfig)
Contract
createProofObl
in interface Contract
public ProofOblInput getProofObl(Services services)
Contract
getProofObl
in interface Contract
public ProofOblInput createProofObl(InitConfig initConfig, Contract contract)
Contract
createProofObl
in interface Contract
public final ProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean addSymbolicExecutionLabel)
Contract
createProofObl
in interface Contract
public String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public String getPODisplayName()
InformationFlowContract
getPODisplayName
in interface InformationFlowContract
public VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
public boolean transactionApplicableContract()
transactionApplicableContract
in interface Contract
public KeYJavaType getSpecifiedIn()
getSpecifiedIn
in interface InformationFlowContract
public InformationFlowContract setID(int newId)
InformationFlowContract
setID
in interface Contract
setID
in interface InformationFlowContract
public InformationFlowContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
InformationFlowContract
setTarget
in interface Contract
setTarget
in interface InformationFlowContract
public InformationFlowContract setName(String name)
setName
in interface InformationFlowContract
public InformationFlowContract setModality(Modality modality)
setModality
in interface InformationFlowContract
public InformationFlowContract setModifies(Term modifies)
setModifies
in interface InformationFlowContract
public Term getDep()
InformationFlowContract
getDep
in interface InformationFlowContract
public ImmutableList<InfFlowSpec> getInfFlowSpecs()
InformationFlowContract
getInfFlowSpecs
in interface InformationFlowContract
public boolean equals(Contract c)
equals
in interface InformationFlowContract
public boolean toBeSaved()
Contract
public String proofToString(Services services)
Contract
proofToString
in interface Contract
public String getPlainText(Services services)
Contract
getPlainText
in interface Contract
public Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
getGlobalDefs
in interface Contract
public boolean hasSelfVar()
Contract
hasSelfVar
in interface Contract
true
self variable is originally provided,
false
no self variable available.@Deprecated public Term getPre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
@Deprecated public Term getPre(List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
@Deprecated public Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
Contract
@Deprecated public Term getPre(List<LocationVariable> heapContext, Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
@Deprecated public Term getMby(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
Contract
@Deprecated public Term getMby(Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
Contract
public Contract.OriginalVariables getOrigVars()
Contract
getOrigVars
in interface Contract
public Term getDep(LocationVariable heap, boolean atPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
public Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
Contract
public Term getRequires(LocationVariable heap)
getRequires
in interface Contract
public Term getAssignable(LocationVariable heap)
getAssignable
in interface Contract
public Term getAccessible(ProgramVariable heap)
getAccessible
in interface Contract
public Term getGlobalDefs()
getGlobalDefs
in interface Contract