public final class ClassWellDefinedness extends WellDefinednessCheck
WellDefinednessCheck.Condition, WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc, WellDefinednessCheck.Type
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
private ClassInvariant |
inv |
INV_TACLET, OP_EXC_TACLET, OP_TACLET, TB
INVALID_ID
Modifier | Constructor and Description |
---|---|
|
ClassWellDefinedness(ClassInvariant inv,
IObserverFunction target,
Term accessible,
Term mby,
Services services) |
private |
ClassWellDefinedness(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,
ClassInvariant inv,
TermBuilder tb) |
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.
|
(package private) Function |
generateMbyAtPreFunc(Services services) |
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.
|
(package private) ImmutableList<Term> |
getRest()
Collects all remaining (implicitly or explicity) specified clauses
(except for pre-condition, post-condition and assignable-clause).
|
java.lang.String |
getTypeName()
Returns technical name for the contract type.
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
boolean |
modelField()
Detects if the specification element is a true (i.e. not an invariant) model field
|
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() |
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 ClassInvariant inv
private ClassWellDefinedness(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, ClassInvariant inv, TermBuilder tb)
public ClassWellDefinedness(ClassInvariant inv, IObserverFunction target, Term accessible, Term mby, Services services)
Function generateMbyAtPreFunc(Services services)
generateMbyAtPreFunc
in class WellDefinednessCheck
ImmutableList<Term> getRest()
WellDefinednessCheck
getRest
in class WellDefinednessCheck
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