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
The jml block contract.
|
INV_TACLET, OP_EXC_TACLET, OP_TACLET, TB
INVALID_ID
Modifier | Constructor and Description |
---|---|
|
BlockWellDefinedness(BlockContract block,
AuxiliaryContract.Variables variables,
ImmutableSet<ProgramVariable> params,
Services services)
Creates a contract to check well-definedness of a block contract
|
private |
BlockWellDefinedness(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,
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() |
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 BlockContract block
private BlockWellDefinedness(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, BlockContract block, TermBuilder tb)
public BlockWellDefinedness(BlockContract block, AuxiliaryContract.Variables variables, ImmutableSet<ProgramVariable> params, Services services)
block
- the block belonging to the block contractvariables
- the variables of the block contractparams
- the parameters of the blockservices
- the services instanceSequentFormula 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
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 BlockWellDefinedness combine(WellDefinednessCheck wdc, TermServices services)
WellDefinednessCheck
combine
in class WellDefinednessCheck
wdc
- the well-definedness check to be combined with the current one