public class LoopWellDefinedness extends StatementWellDefinedness
StatementWellDefinedness.SequentTerms
WellDefinednessCheck.Condition, WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc, WellDefinednessCheck.Type
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
private LoopSpecification |
inv |
INV_TACLET, OP_EXC_TACLET, OP_TACLET, TB
INVALID_ID
Modifier | Constructor and Description |
---|---|
|
LoopWellDefinedness(LoopSpecification inv,
ImmutableSet<ProgramVariable> params,
Services services) |
private |
LoopWellDefinedness(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,
LoopSpecification 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.
|
LoopSpecification |
getStatement() |
java.lang.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
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
isAuxiliary
private final LoopSpecification inv
private LoopWellDefinedness(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, LoopSpecification inv, TermBuilder tb)
public LoopWellDefinedness(LoopSpecification inv, ImmutableSet<ProgramVariable> params, Services services)
SequentFormula generateSequent(StatementWellDefinedness.SequentTerms seq, TermServices services)
StatementWellDefinedness
generateSequent
in class StatementWellDefinedness
public LoopSpecification getStatement()
getStatement
in class StatementWellDefinedness
public boolean transactionApplicableContract()
public Contract setID(int newId)
Contract
newId
- the new id valuepublic Contract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
Contract
newKJT
- the new KeYJavaTypenewPM
- the new observer functionpublic java.lang.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