public class LoopWellDefinedness extends StatementWellDefinedness
StatementWellDefinedness.SequentTerms
WellDefinednessCheck.Condition, WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc, WellDefinednessCheck.Type
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
private LoopInvariant |
inv |
INV_TACLET, OP_EXC_TACLET, OP_TACLET, TB
INVALID_ID
Modifier | Constructor and Description |
---|---|
|
LoopWellDefinedness(LoopInvariant inv,
ImmutableSet<ProgramVariable> params,
Services services) |
private |
LoopWellDefinedness(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,
LoopInvariant inv,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
LoopWellDefinedness |
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.
|
(package private) SequentFormula |
generateSequent(StatementWellDefinedness.SequentTerms seq,
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.
|
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
LoopInvariant |
getStatement() |
String |
getTypeName()
Returns technical name for the contract type.
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
Contract |
setID(int newId)
Returns a contract which is identical this contract except that
the id is set to the new id.
|
Contract |
setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Returns a contract which is identical to this contract except that
the KeYJavaType and IObserverFunction are set to the new values.
|
boolean |
transactionApplicableContract() |
convertParams, createSeqTerms, generateMbyAtPreFunc, generateSequent, generateSequent, getAxiom, getBehaviour, getGlobalDefs, getRest, modelField
addEnsures, addEnsures, addRepresents, addRequires, addRequires, 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
private final LoopInvariant inv
private LoopWellDefinedness(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, LoopInvariant inv, TermBuilder tb)
public LoopWellDefinedness(LoopInvariant inv, ImmutableSet<ProgramVariable> params, Services services)
SequentFormula generateSequent(StatementWellDefinedness.SequentTerms seq, TermServices services)
StatementWellDefinedness
generateSequent
in class StatementWellDefinedness
public LoopInvariant getStatement()
getStatement
in class StatementWellDefinedness
public boolean transactionApplicableContract()
public Contract setID(int newId)
Contract
public Contract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
Contract
public String getTypeName()
Contract
public VisibilityModifier getVisibility()
SpecificationElement
public KeYJavaType getKJT()
SpecificationElement
public LoopWellDefinedness combine(WellDefinednessCheck wdc, TermServices services)
WellDefinednessCheck
combine
in class WellDefinednessCheck
wdc
- the well-definedness check to be combined with the current one