public abstract class StatementWellDefinedness extends WellDefinednessCheck
#generateSequent(ProgramVariable, ProgramVariable, ProgramVariable, LocationVariable,
ProgramVariable, Term, ImmutableSet, Term, Services)
Nevertheless it is imaginable to make them separate contracts.WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc
Contract.OriginalVariables
INV_TACLET, OP_EXC_TACLET, OP_TACLET
INVALID_ID
Modifier and Type | Method and Description |
---|---|
SequentFormula |
generateSequent(ProgramVariable self,
LocationVariable heap,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built, however with a smaller set of variables,
due to the nature of the jml statement.
|
SequentFormula |
generateSequent(ProgramVariable self,
ProgramVariable exception,
ProgramVariable result,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built.
|
Term |
getAxiom()
Only for contracts with model_behaviour, the result is different from null.
|
java.lang.String |
getBehaviour()
Detects the specification element's behaviour
|
Term |
getGlobalDefs() |
abstract SpecificationElement |
getStatement() |
abstract StatementWellDefinedness |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
boolean |
modelField()
Detects if the specification element is a true (i.e.
|
addRepresents, combine, createPOTerms, createProofObl, createProofObl, createProofObl, equals, getAccessible, getAccessible, getAssignable, getAssignable, getDep, getDep, getDisplayName, getEnsures, getEnsures, getGlobalDefs, getHeap, getHTMLText, getMby, getMby, getMby, getName, getOrigVars, getPlainText, getPost, getPre, getPre, getPre, getPre, getPre, getProofObl, getRepresents, getRequires, getRequires, getTarget, getUpdates, hashCode, hasMby, hasSelfVar, id, isConstructor, isOn, name, proofToString, replace, replace, toBeSaved, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getTypeName, isAuxiliary, setID, setTarget, transactionApplicableContract
getKJT, getVisibility
public abstract SpecificationElement getStatement()
public SequentFormula generateSequent(ProgramVariable self, ProgramVariable exception, ProgramVariable result, LocationVariable heap, ProgramVariable heapAtPre, Term anonHeap, ImmutableSet<ProgramVariable> ps, Term leadingUpdate, Term localAnonUpdate, Services services)
self
- The current self variableexception
- The current exception variableresult
- The current result variableheap
- The current heapheapAtPre
- The current old heapanonHeap
- The anonymized heapps
- The current parameter variablesleadingUpdate
- The context updatelocalAnonUpdate
- anonymization update of local variablesservices
- The current services referencepublic SequentFormula generateSequent(ProgramVariable self, LocationVariable heap, Term anonHeap, ImmutableSet<ProgramVariable> ps, Term leadingUpdate, Term localAnonUpdate, Services services)
self
- self variableheap
- heap variableanonHeap
- anonymised heapps
- set of parameter variablesleadingUpdate
- the context updatelocalAnonUpdate
- anonymization update of local variablesservices
- public abstract StatementWellDefinedness map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface Contract
map
in interface SpecificationElement
map
in class WellDefinednessCheck
op
- the operator to apply.services
- services.public final java.lang.String getBehaviour()
WellDefinednessCheck
getBehaviour
in class WellDefinednessCheck
public final Term getGlobalDefs()
public final Term getAxiom()
WellDefinednessCheck
getAxiom
in class WellDefinednessCheck
public final boolean modelField()
WellDefinednessCheck
modelField
in class WellDefinednessCheck
Copyright © 2003-2019 The KeY-Project.