public class BlockWellDefinedness extends StatementWellDefinedness
StatementWellDefinedness.SequentTerms
WellDefinednessCheck.Condition, WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc, WellDefinednessCheck.Type
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
private BlockContract |
block |
INV_TACLET, OP_EXC_TACLET, OP_TACLET, TB
INVALID_ID
Modifier | Constructor and Description |
---|---|
|
BlockWellDefinedness(BlockContract block,
ImmutableSet<ProgramVariable> params,
Services services) |
private |
BlockWellDefinedness(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,
BlockContract block,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
BlockWellDefinedness |
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.
|
BlockContract |
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 BlockContract block
private BlockWellDefinedness(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, BlockContract block, TermBuilder tb)
public BlockWellDefinedness(BlockContract block, ImmutableSet<ProgramVariable> params, Services services)
SequentFormula generateSequent(StatementWellDefinedness.SequentTerms seq, TermServices services)
StatementWellDefinedness
generateSequent
in class StatementWellDefinedness
public BlockContract 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 BlockWellDefinedness combine(WellDefinednessCheck wdc, TermServices services)
WellDefinednessCheck
combine
in class WellDefinednessCheck
wdc
- the well-definedness check to be combined with the current one