public final class InformationFlowContractImpl extends java.lang.Object implements InformationFlowContract
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
private java.lang.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 java.lang.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(java.lang.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(java.lang.String baseName,
java.lang.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 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() |
java.lang.String |
getBaseName() |
Term |
getDep()
Returns the dependency set of the contract.
|
Term |
getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.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,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the dependency set of the contract.
|
java.lang.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) |
java.lang.String |
getHTMLBody(Services services) |
private java.lang.String |
getHTMLFor(ImmutableList<InfFlowSpec> originalInfFlowSpecs,
java.lang.String htmlName,
Services services) |
private java.lang.String |
getHTMLFor(java.lang.Iterable<Term> originalTerms,
Services services) |
protected java.lang.String |
getHTMLFor(Term originalTerm,
java.lang.String htmlName,
Services services) |
private java.lang.String |
getHTMLSignature() |
private java.lang.StringBuffer |
getHTMLSignatureBody() |
java.lang.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(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.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.
|
java.lang.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.
|
java.lang.String |
getPlainText(Services services)
Returns the contract in pretty plain text format.
|
java.lang.String |
getPODisplayName()
For generating contract name of SymbolicExecutionPO
|
Term |
getPre()
Returns the original precondition of the contract.
|
Term |
getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.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.
|
java.lang.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() |
java.lang.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(java.lang.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.
|
java.lang.String |
toString() |
boolean |
transactionApplicableContract() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
isAuxiliary
private final int id
private final KeYJavaType forClass
private final IProgramMethod pm
private final KeYJavaType specifiedIn
private final java.lang.String baseName
private final java.lang.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(java.lang.String baseName, java.lang.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(java.lang.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 java.lang.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 java.lang.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 java.lang.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 java.lang.String getHTMLText(Services services)
Contract
getHTMLText
in interface Contract
services
- services instancepublic java.lang.String getHTMLBody(Services services)
private java.lang.String getHTMLSignature()
private java.lang.StringBuffer getHTMLSignatureBody()
protected java.lang.String getHTMLFor(Term originalTerm, java.lang.String htmlName, Services services)
private java.lang.String getHTMLFor(java.lang.Iterable<Term> originalTerms, Services services)
private java.lang.String getHTMLFor(ImmutableList<InfFlowSpec> originalInfFlowSpecs, java.lang.String htmlName, Services services)
public java.lang.String toString()
toString
in class java.lang.Object
public final ContractPO createProofObl(InitConfig initConfig)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationpublic ProofOblInput getProofObl(Services services)
Contract
getProofObl
in interface Contract
services
- the services instancepublic ProofOblInput createProofObl(InitConfig initConfig, Contract contract)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationcontract
- the contractpublic final ProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean addSymbolicExecutionLabel)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationcontract
- the contractaddSymbolicExecutionLabel
- boolean saying whether symbolic execution api is supportedpublic java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public java.lang.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
newId
- the new id valuepublic InformationFlowContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
InformationFlowContract
setTarget
in interface Contract
setTarget
in interface InformationFlowContract
newKJT
- the new KeYJavaTypenewPM
- the new observer functionpublic InformationFlowContract setName(java.lang.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 java.lang.String proofToString(Services services)
Contract
proofToString
in interface Contract
services
- the services instancepublic java.lang.String getPlainText(Services services)
Contract
getPlainText
in interface Contract
services
- services instancepublic 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, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
@Deprecated public Term getPre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
@Deprecated public Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
Contract
@Deprecated public Term getPre(java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
Contract
@Deprecated public Term getMby(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
Contract
@Deprecated public Term getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.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, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
public Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
Contract
getDep
in interface Contract
heap
- the heap variableatPre
- boolean whether old heap should be usedheapTerm
- the heap variable termselfTerm
- term of self variableparamTerms
- terms of parameter variablesatPres
- terms of variables at previous heapservices
- services objectpublic 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