T
- the type of AuxiliaryContract
for which this class generated POs.public abstract class FunctionalAuxiliaryContract<T extends AuxiliaryContract> extends java.lang.Object implements Contract
AuxiliaryContract
.Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
private T |
contract |
private java.lang.String |
displayName
This contract's display name.
|
private int |
id
This contract's ID.
|
private java.lang.String |
name
This contract's name.
|
private java.lang.String |
typeName
This contract's type name.
|
INVALID_ID
Constructor and Description |
---|
FunctionalAuxiliaryContract(T contract) |
FunctionalAuxiliaryContract(T contract,
int id) |
Modifier and Type | Method and Description |
---|---|
ProofOblInput |
createProofObl(InitConfig initConfig,
Contract contract)
Returns a proof obligation to the passed contract and initConfig.
|
ProofOblInput |
createProofObl(InitConfig initConfig,
Contract contract,
boolean supportSymbolicExecutionAPI)
Returns a proof obligation to the passed contract and initConfig.
|
private java.lang.String |
generateName(java.lang.String baseName,
java.util.function.UnaryOperator<java.lang.String> generator) |
Term |
getAccessible(ProgramVariable heap) |
Term |
getAssignable(LocationVariable heap) |
T |
getAuxiliaryContract() |
StatementBlock |
getBlock() |
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 |
getGlobalDefs() |
Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
java.lang.String |
getHTMLText(Services services)
Returns the contract in pretty HTML format.
|
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
Term |
getMby() |
Term |
getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the measured_by clause of the contract.
|
Term |
getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the measured_by clause of the contract.
|
IProgramMethod |
getMethod() |
Modality |
getModality() |
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original ProgramVariables to replace them easier.
|
AuxiliaryContract.Variables |
getPlaceholderVariables()
Returns the set of placeholder variables created during this contract's instantiation.
|
java.lang.String |
getPlainText(Services services)
Returns the contract in pretty plain text format.
|
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)
Returns the precondition of the contract.
|
Term |
getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
Term |
getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
Term |
getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
ProofOblInput |
getProofObl(Services services)
Lookup the proof obligation belonging to the contract in the specification repository.
|
Term |
getRequires(LocationVariable heap) |
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 |
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 |
hasSelfVar()
Checks if a self variable is originally provided.
|
int |
id()
Returns the id number of the contract.
|
boolean |
isAuxiliary() |
java.lang.String |
proofToString(Services services)
Returns a parseable String representation of the contract.
|
protected void |
setAuxiliaryContract(T contract) |
boolean |
toBeSaved()
Tells whether, on saving a proof where this contract is available, the contract should be
saved too.
|
boolean |
transactionApplicableContract() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
createProofObl, setID, setTarget
private T extends AuxiliaryContract contract
getAuxiliaryContract()
private final int id
private final java.lang.String name
private final java.lang.String displayName
private final java.lang.String typeName
FunctionalAuxiliaryContract(T contract)
contract
- a block contract.FunctionalAuxiliaryContract(T contract, int id)
contract
- a block contract.id
- an ID.private java.lang.String generateName(java.lang.String baseName, java.util.function.UnaryOperator<java.lang.String> generator)
baseName
- a base name.generator
- a name generator.public boolean isAuxiliary()
isAuxiliary
in interface Contract
true
if any only if this contract does not necessarily need to be proven in
its own proof obligation. E.g., this is true for FunctionalBlockContract
s and
FunctionalLoopContract
s.public java.lang.String getName()
SpecificationElement
getName
in interface SpecificationElement
public java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
public int id()
Contract
public IProgramMethod getTarget()
Contract
public boolean hasMby()
Contract
public Term getMby(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
Contract
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 getPre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
public Term getPre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
public Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
Contract
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
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
public Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
getGlobalDefs
in interface Contract
public java.lang.String getHTMLText(Services services)
Contract
getHTMLText
in interface Contract
services
- services instancepublic java.lang.String getPlainText(Services services)
Contract
getPlainText
in interface Contract
services
- services instancepublic boolean toBeSaved()
Contract
public boolean transactionApplicableContract()
transactionApplicableContract
in interface Contract
public java.lang.String proofToString(Services services)
Contract
proofToString
in interface Contract
services
- the services instancepublic 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 ProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean supportSymbolicExecutionAPI)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationcontract
- the contractsupportSymbolicExecutionAPI
- boolean saying whether symbolic execution api is supportedpublic java.lang.String getTypeName()
Contract
getTypeName
in interface Contract
public boolean hasSelfVar()
Contract
hasSelfVar
in interface Contract
true
self variable is originally provided, false
no self variable
available.public boolean hasModifiesClause(LocationVariable heap)
true
iff the method (according to the contract) does not modify the heap
at all, i.e., iff it is "strictly pure."heap
- the heap to use.true
iff this contract is strictly pure.AuxiliaryContract.hasModifiesClause(LocationVariable)
protected void setAuxiliaryContract(T contract)
public T getAuxiliaryContract()
AuxiliaryContract
.public StatementBlock getBlock()
AuxiliaryContract.getBlock()
public IProgramMethod getMethod()
getBlock()
AuxiliaryContract.getMethod()
public AuxiliaryContract.Variables getPlaceholderVariables()
AuxiliaryContractBuilders.VariablesCreatorAndRegistrar
,
AuxiliaryContract.getPlaceholderVariables()
public Modality getModality()
AuxiliaryContract.getModality()