public final class MethodWellDefinedness extends WellDefinednessCheck
WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc
Contract.OriginalVariables
INV_TACLET, OP_EXC_TACLET, OP_TACLET
INVALID_ID
Constructor and Description |
---|
MethodWellDefinedness(DependencyContract contract,
Services services) |
MethodWellDefinedness(FunctionalOperationContract contract,
Services services) |
MethodWellDefinedness(RepresentsAxiom rep,
Services services) |
Modifier and Type | Method and Description |
---|---|
MethodWellDefinedness |
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.
|
RewriteTaclet |
combineTaclets(RewriteTaclet t1,
RewriteTaclet t2,
TermServices services)
Combines two well-definedness taclets for (pure) method invocations.
|
RewriteTaclet |
createOperationTaclet(Services services)
Creates a well-definedness for a (pure) method invocation of this method.
|
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() |
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
Contract |
getMethodContract() |
java.lang.String |
getTypeName()
Returns technical name for the contract type.
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
boolean |
isModel()
Tells whether the method is a model method, i.e.
|
boolean |
isNormal(TermServices services)
Used to determine if the contract of this method has normal behaviour or
is a model field/method and can thus not throw any exception.
|
boolean |
isPure()
Tells whether the method is pure or not.
|
MethodWellDefinedness |
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.
|
MethodWellDefinedness |
setID(int newId)
Returns a contract which is identical this contract except that the id is set to the new id.
|
MethodWellDefinedness |
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 MethodWellDefinedness(FunctionalOperationContract contract, Services services)
public MethodWellDefinedness(DependencyContract contract, Services services)
public MethodWellDefinedness(RepresentsAxiom rep, Services services)
public MethodWellDefinedness 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 Contract getMethodContract()
public RewriteTaclet createOperationTaclet(Services services)
services
- public RewriteTaclet combineTaclets(RewriteTaclet t1, RewriteTaclet t2, TermServices services)
t1
- taclet onet2
- taclet twoservices
- public java.lang.String getBehaviour()
WellDefinednessCheck
getBehaviour
in class WellDefinednessCheck
public boolean isNormal(TermServices services)
public boolean isPure()
public boolean isModel()
public boolean modelField()
WellDefinednessCheck
modelField
in class WellDefinednessCheck
public MethodWellDefinedness combine(WellDefinednessCheck wdc, TermServices services)
WellDefinednessCheck
combine
in class WellDefinednessCheck
wdc
- the well-definedness check to be combined with the current onepublic Term getGlobalDefs()
public Term getAxiom()
WellDefinednessCheck
getAxiom
in class WellDefinednessCheck
public boolean transactionApplicableContract()
public MethodWellDefinedness setID(int newId)
Contract
newId
- the new id valuepublic MethodWellDefinedness 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
Copyright © 2003-2019 The KeY-Project.