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.Modifier and Type | Class and Description |
---|---|
(package private) class |
StatementWellDefinedness.SequentTerms
A data structure to pass the needed terms for the well-definedness sequent of a jml
statement, including the context update, pre-condition for the statement, well-formedness
condition for the anonymous heap, well-definedness term for the statement's assignable-clause,
well-definedness term for other clauses in the statement and the well-definedness term for
the statement's post-condition with the according updates (heap of pre-state becomes current
heap and the current heap gets anonymised) applied to it.
|
WellDefinednessCheck.Condition, WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc, WellDefinednessCheck.Type
Contract.OriginalVariables
INV_TACLET, OP_EXC_TACLET, OP_TACLET, TB
INVALID_ID
Constructor and Description |
---|
StatementWellDefinedness(java.lang.String name,
int id,
IObserverFunction target,
Contract.OriginalVariables origVars,
WellDefinednessCheck.Type type,
Services services) |
StatementWellDefinedness(java.lang.String name,
int id,
WellDefinednessCheck.Type type,
IObserverFunction target,
LocationVariable heap,
Contract.OriginalVariables origVars,
WellDefinednessCheck.Condition requires,
Term assignable,
Term accessible,
WellDefinednessCheck.Condition ensures,
Term mby,
Term rep,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
(package private) static ImmutableList<ProgramVariable> |
convertParams(ImmutableSet<ProgramVariable> set)
Converts a set of parameter variables into a list of parameter variables
|
(package private) StatementWellDefinedness.SequentTerms |
createSeqTerms(WellDefinednessCheck.POTerms po,
WellDefinednessPO.Variables vars,
Term leadingUpdate,
Term localAnon,
Services services)
Aggregates and preprocesses the proof obligation data into the according terms for the
well-definedness sequent of the jml statement.
|
(package private) Function |
generateMbyAtPreFunc(Services services) |
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.
|
(package private) abstract SequentFormula |
generateSequent(StatementWellDefinedness.SequentTerms seqTerms,
TermServices services)
This formula creates the sequent formula for the well-definedness of a jml statement
in the specific way, in which it is required for the specific jml statement.
|
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() |
(package private) ImmutableList<Term> |
getRest()
Collects all remaining (implicitly or explicity) specified clauses
(except for pre-condition, post-condition and assignable-clause).
|
abstract SpecificationElement |
getStatement() |
boolean |
modelField()
Detects if the specification element is a true (i.e. not an invariant) model field
|
addEnsures, addEnsures, addRepresents, addRequires, addRequires, combine, combineAccessible, combineAssignable, createExcTaclet, createPOTerms, createProofObl, createProofObl, createProofObl, createTaclet, createTaclet, 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, replace, replaceSV, setAccessible, setAssignable, setEnsures, setMby, setRequires, toBeSaved, toString, type
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getTypeName, isAuxiliary, setID, setTarget, transactionApplicableContract
getKJT, getVisibility
StatementWellDefinedness(java.lang.String name, int id, IObserverFunction target, Contract.OriginalVariables origVars, WellDefinednessCheck.Type type, Services services)
StatementWellDefinedness(java.lang.String name, int id, WellDefinednessCheck.Type type, IObserverFunction target, LocationVariable heap, Contract.OriginalVariables origVars, WellDefinednessCheck.Condition requires, Term assignable, Term accessible, WellDefinednessCheck.Condition ensures, Term mby, Term rep, TermBuilder tb)
abstract SequentFormula generateSequent(StatementWellDefinedness.SequentTerms seqTerms, TermServices services)
seqTerms
- services
- public abstract SpecificationElement getStatement()
static final ImmutableList<ProgramVariable> convertParams(ImmutableSet<ProgramVariable> set)
set
- a set of parameter variablesfinal Function generateMbyAtPreFunc(Services services)
generateMbyAtPreFunc
in class WellDefinednessCheck
final ImmutableList<Term> getRest()
WellDefinednessCheck
getRest
in class WellDefinednessCheck
final StatementWellDefinedness.SequentTerms createSeqTerms(WellDefinednessCheck.POTerms po, WellDefinednessPO.Variables vars, Term leadingUpdate, Term localAnon, Services services)
po
- the proof obligation terms of the statementvars
- the new (current) variablesleadingUpdate
- the context update of the program before the statementlocalAnon
- anonymize local variablesservices
- 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 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