public abstract class WellDefinednessCheck extends java.lang.Object implements Contract
Modifier and Type | Class and Description |
---|---|
static class |
WellDefinednessCheck.POTerms
A data structure for storing and passing all specifications of a
specification element includinf pre- and post-condition, an
assignable-clause and a list of all other clauses specified.
|
static class |
WellDefinednessCheck.TermAndFunc
A static data structure for passing a term with a function.
|
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
INV_TACLET |
static java.lang.String |
OP_EXC_TACLET |
static java.lang.String |
OP_TACLET |
INVALID_ID
Modifier and Type | Method and Description |
---|---|
WellDefinednessCheck |
addRepresents(Term rep) |
WellDefinednessCheck |
combine(WellDefinednessCheck wdc,
TermServices services)
Combines two well-definedness checks having the same name, id, target, type,
behaviour and are either both model fields or both not a model field.
|
WellDefinednessCheck.POTerms |
createPOTerms()
collects terms for precondition,
assignable clause and other specification elements,
and postcondition & signals-clause
|
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(java.lang.Object o) |
Term |
getAccessible() |
Term |
getAccessible(ProgramVariable heap) |
Term |
getAssignable() |
Term |
getAssignable(LocationVariable heap) |
abstract Term |
getAxiom()
Only for contracts with model_behaviour, the result is different from null.
|
abstract java.lang.String |
getBehaviour()
Detects the specification element's behaviour
|
Term |
getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
java.lang.String |
getDisplayName()
Returns the displayed name.
|
de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition |
getEnsures() |
Term |
getEnsures(LocationVariable heap) |
Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Deprecated.
|
LocationVariable |
getHeap() |
java.lang.String |
getHTMLText(Services services)
Returns the contract in pretty HTML format.
|
Term |
getMby() |
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.
|
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original ProgramVariables to replace them easier.
|
java.lang.String |
getPlainText(Services services)
Returns the contract in pretty plain text format.
|
Term |
getPost(de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition post,
ParsableVariable result,
TermServices services)
Gets the full valid post-condition
|
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.
|
WellDefinednessCheck.TermAndFunc |
getPre(de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition pre,
ParsableVariable self,
ParsableVariable heap,
ImmutableList<? extends ParsableVariable> parameters,
boolean taclet,
Services services)
Gets the full valid precondition, which holds in the element's pre-state.
|
ProofOblInput |
getProofObl(Services services)
Lookup the proof obligation belonging to the contract in the specification repository.
|
Term |
getRepresents() |
de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition |
getRequires() |
Term |
getRequires(LocationVariable heap) |
IObserverFunction |
getTarget()
Returns the contracted function symbol.
|
Term |
getUpdates(Term mod,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
TermServices services)
Gets the necessary updates applicable to the post-condition
|
int |
hashCode() |
boolean |
hasMby()
Tells whether the contract contains a measured_by clause.
|
boolean |
hasSelfVar()
Checks if a self variable is originally provided.
|
int |
id()
Returns the id number of the contract.
|
boolean |
isConstructor() |
static boolean |
isOn()
This method checks, if well-definedness checks are generally turned on or off.
|
abstract WellDefinednessCheck |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
abstract boolean |
modelField()
Detects if the specification element is a true (i.e.
|
Name |
name() |
java.lang.String |
proofToString(Services services)
Returns a parseable String representation of the contract.
|
Term |
replace(Term t,
WellDefinednessPO.Variables vars) |
WellDefinednessCheck.POTerms |
replace(WellDefinednessCheck.POTerms po,
WellDefinednessPO.Variables vars) |
boolean |
toBeSaved()
Tells whether, on saving a proof where this contract is available, the contract should be
saved too.
|
java.lang.String |
toString() |
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getGlobalDefs, getTypeName, isAuxiliary, setID, setTarget, transactionApplicableContract
getKJT, getVisibility
public static final java.lang.String INV_TACLET
public static final java.lang.String OP_TACLET
public static final java.lang.String OP_EXC_TACLET
public abstract WellDefinednessCheck map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface Contract
map
in interface SpecificationElement
op
- the operator to apply.services
- services.public abstract java.lang.String getBehaviour()
public abstract boolean modelField()
public abstract Term getAxiom()
public WellDefinednessCheck combine(WellDefinednessCheck wdc, TermServices services)
wdc
- the well-definedness check to be combined with the current oneservices
- public static final boolean isOn()
public final WellDefinednessCheck.POTerms createPOTerms()
public final WellDefinednessCheck addRepresents(Term rep)
public final WellDefinednessCheck.TermAndFunc getPre(de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition pre, ParsableVariable self, ParsableVariable heap, ImmutableList<? extends ParsableVariable> parameters, boolean taclet, Services services)
pre
- the precondition with the original variablesself
- the new self variableheap
- the new heap variableparameters
- the new parameter listtaclet
- is true if the precondition will be used in a tacletservices
- public final Term getPost(de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition post, ParsableVariable result, TermServices services)
post
- post-condition with original variablesresult
- the new result variableservices
- public final Term getUpdates(Term mod, LocationVariable heap, ProgramVariable heapAtPre, Term anonHeap, TermServices services)
mod
- the assignable-clauseheap
- the current heap variableheapAtPre
- the current variable for the heap of the pre-stateanonHeap
- the anonymous heap termservices
- public final Term replace(Term t, WellDefinednessPO.Variables vars)
public final WellDefinednessCheck.POTerms replace(WellDefinednessCheck.POTerms po, WellDefinednessPO.Variables vars)
public final LocationVariable getHeap()
public final Name name()
public final de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition getRequires()
public final Term getAssignable()
public final Term getAccessible()
public final de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition getEnsures()
public final Term getEnsures(LocationVariable heap)
public final Term getRepresents()
public final boolean isConstructor()
public final java.lang.String toString()
toString
in class java.lang.Object
public final java.lang.String getName()
SpecificationElement
getName
in interface SpecificationElement
public final int id()
Contract
public final boolean hasMby()
Contract
public final Term getRequires(LocationVariable heap)
getRequires
in interface Contract
public final Term getAssignable(LocationVariable heap)
getAssignable
in interface Contract
public final Term getAccessible(ProgramVariable heap)
getAccessible
in interface Contract
public final java.lang.String getHTMLText(Services services)
Contract
getHTMLText
in interface Contract
services
- services instancepublic final java.lang.String getPlainText(Services services)
Contract
getPlainText
in interface Contract
services
- services instancepublic final java.lang.String proofToString(Services services)
Contract
proofToString
in interface Contract
services
- the services instancepublic final IObserverFunction getTarget()
Contract
public final 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 final ContractPO createProofObl(InitConfig initConfig)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationpublic final ProofOblInput getProofObl(Services services)
Contract
getProofObl
in interface Contract
services
- the services instancepublic final java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public final boolean toBeSaved()
Contract
public final boolean hasSelfVar()
Contract
hasSelfVar
in interface Contract
true
self variable is originally provided, false
no self variable
available.public final Contract.OriginalVariables getOrigVars()
Contract
getOrigVars
in interface Contract
public final boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public final int hashCode()
hashCode
in class java.lang.Object
@Deprecated public final Term getPre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services) throws java.lang.UnsupportedOperationException
Contract
@Deprecated public final Term getPre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services) throws java.lang.UnsupportedOperationException
Contract
@Deprecated public final Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services) throws java.lang.UnsupportedOperationException
Contract
@Deprecated public final 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) throws java.lang.UnsupportedOperationException
Contract
getPre
in interface Contract
heapContext
- heap contextheapTerms
- heap termsselfTerm
- term of self variableparamTerms
- terms of parameter variablesatPres
- terms of variables at previous heapservices
- services objectjava.lang.UnsupportedOperationException
@Deprecated public final Term getDep(LocationVariable heap, boolean atPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
@Deprecated public final 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 object@Deprecated public final Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
getGlobalDefs
in interface Contract
@Deprecated public final Term getMby(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services) throws java.lang.UnsupportedOperationException
Contract
@Deprecated public final Term getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services) throws java.lang.UnsupportedOperationException
Contract
getMby
in interface Contract
heapTerms
- terms for the heap contextselfTerm
- term of self variableparamTerms
- terms of parameter variablesatPres
- terms of variables at previous heapservices
- services objectjava.lang.UnsupportedOperationException
Copyright © 2003-2019 The KeY-Project.