public final class ClassWellDefinedness extends WellDefinednessCheck
WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc
Contract.OriginalVariables
INV_TACLET, OP_EXC_TACLET, OP_TACLET
INVALID_ID
Constructor and Description |
---|
ClassWellDefinedness(ClassInvariant inv,
IObserverFunction target,
Term accessible,
Term mby,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
addInv(Term inv) |
ClassWellDefinedness |
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.
|
static ImmutableSet<RewriteTaclet> |
createInvTaclet(Services services)
Creates a well-definedness taclet for an invariant reference.
|
Term |
getAxiom()
Only for contracts with model_behaviour, the result is different from null.
|
java.lang.String |
getBehaviour()
Detects the specification element's behaviour
|
Term |
getGlobalDefs() |
ClassInvariant |
getInvariant() |
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
java.lang.String |
getTypeName()
Returns technical name for the contract type.
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
ClassWellDefinedness |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
boolean |
modelField()
Detects if the specification element is a true (i.e.
|
ClassWellDefinedness |
setID(int newId)
Returns a contract which is identical this contract except that the id is set to the new id.
|
ClassWellDefinedness |
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() |
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 ClassWellDefinedness(ClassInvariant inv, IObserverFunction target, Term accessible, Term mby, Services services)
public ClassWellDefinedness map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface Contract
map
in interface SpecificationElement
map
in class WellDefinednessCheck
op
- the operator to apply.services
- services.public static ImmutableSet<RewriteTaclet> createInvTaclet(Services services)
services
- public ClassInvariant getInvariant()
public final void addInv(Term inv)
public java.lang.String getBehaviour()
WellDefinednessCheck
getBehaviour
in class WellDefinednessCheck
public boolean modelField()
WellDefinednessCheck
modelField
in class WellDefinednessCheck
public ClassWellDefinedness combine(WellDefinednessCheck wdc, TermServices services)
WellDefinednessCheck
combine
in class WellDefinednessCheck
wdc
- the well-definedness check to be combined with the current onepublic boolean transactionApplicableContract()
public ClassWellDefinedness setID(int newId)
Contract
newId
- the new id valuepublic ClassWellDefinedness 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 Term getGlobalDefs()
public Term getAxiom()
WellDefinednessCheck
getAxiom
in class WellDefinednessCheck
Copyright © 2003-2019 The KeY-Project.