public class BlockWellDefinedness extends StatementWellDefinedness
WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc
Contract.OriginalVariables
INV_TACLET, OP_EXC_TACLET, OP_TACLET
INVALID_ID
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
|
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.
|
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)
|
BlockWellDefinedness |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
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() |
generateSequent, generateSequent, getAxiom, getBehaviour, getGlobalDefs, modelField
addRepresents, createPOTerms, createProofObl, createProofObl, createProofObl, 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, toBeSaved, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
isAuxiliary
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 instancepublic BlockWellDefinedness map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface Contract
map
in interface SpecificationElement
map
in class StatementWellDefinedness
op
- the operator to apply.services
- services.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 oneCopyright © 2003-2019 The KeY-Project.