public final class MethodWellDefinedness extends WellDefinednessCheck
WellDefinednessCheck.Condition, WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc, WellDefinednessCheck.Type
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
private Term |
axiom |
private Contract |
contract |
private Term |
globalDefs |
private boolean |
modelField |
INV_TACLET, OP_EXC_TACLET, OP_TACLET, TB
INVALID_ID
Modifier | Constructor and Description |
---|---|
|
MethodWellDefinedness(DependencyContract contract,
Services services) |
|
MethodWellDefinedness(FunctionalOperationContract contract,
Services services) |
|
MethodWellDefinedness(RepresentsAxiom rep,
Services services) |
private |
MethodWellDefinedness(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,
Contract contract,
Term globalDefs,
Term axiom,
boolean model,
TermBuilder tb) |
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.
|
private boolean |
findExcNull(Term t,
ProgramVariable exc)
Finds an -on top level- conjuncted term of the form (exc = null) in the given term.
|
(package private) Term |
generateMbyAtPreDef(ParsableVariable self,
ImmutableList<ParsableVariable> params,
Function mbyAtPreFunc,
Services services)
Generates a term of the form (mbyAtPre = mby) if mby is specified.
|
(package private) Function |
generateMbyAtPreFunc(Services services) |
private Term[] |
getArgs(SchemaVariable sv,
ParsableVariable heap,
ParsableVariable heapAtPre,
boolean isStatic,
boolean twoState,
ImmutableList<ParsableVariable> params)
Gets the argument list for the operator of the 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() |
(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 |
isModel()
Tells whether the method is a model method, i.e. has model behaviour or not.
|
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.
|
boolean |
modelField()
Detects if the specification element is a true (i.e. not an invariant) model field
|
private ImmutableList<ParsableVariable> |
paramsSV()
Converts the original parameters into schema variables
|
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() |
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 Contract contract
private Term globalDefs
private Term axiom
private final boolean modelField
private MethodWellDefinedness(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, Contract contract, Term globalDefs, Term axiom, boolean model, TermBuilder tb)
public MethodWellDefinedness(FunctionalOperationContract contract, Services services)
public MethodWellDefinedness(DependencyContract contract, Services services)
public MethodWellDefinedness(RepresentsAxiom rep, Services services)
private Term[] getArgs(SchemaVariable sv, ParsableVariable heap, ParsableVariable heapAtPre, boolean isStatic, boolean twoState, ImmutableList<ParsableVariable> params)
sv
- schema variable for selfheap
- schema variable for the heapisStatic
- information whether this is a static methodparams
- schema variables for the parametersprivate boolean findExcNull(Term t, ProgramVariable exc)
t
- the term to be searched inexc
- the exception variableprivate ImmutableList<ParsableVariable> paramsSV()
Function generateMbyAtPreFunc(Services services)
generateMbyAtPreFunc
in class WellDefinednessCheck
Term generateMbyAtPreDef(ParsableVariable self, ImmutableList<ParsableVariable> params, Function mbyAtPreFunc, Services services)
self
- the self variableparams
- the list of parametersmbyAtPreFunc
- the measured-by functionservices
- ImmutableList<Term> getRest()
WellDefinednessCheck
getRest
in class WellDefinednessCheck
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