public abstract class WellDefinednessCheck extends java.lang.Object implements Contract
Modifier and Type | Class and Description |
---|---|
(package private) static class |
WellDefinednessCheck.Condition
A static data structure for storing and passing two terms, denoting the implicit
and the explicit part of a pre- or post-condition.
|
static class |
WellDefinednessCheck.POTerms
A data structure for storing and passing all specifications of a
specification element includinf pre- and post-condition, an
assignable-clause and a list of all other clauses specified.
|
static class |
WellDefinednessCheck.TermAndFunc
A static data structure for passing a term with a function.
|
private static class |
WellDefinednessCheck.TermListAndFunc
A static data structure for passing a term list with a function.
|
(package private) static class |
WellDefinednessCheck.Type |
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
private Term |
accessible |
private Term |
assignable |
private WellDefinednessCheck.Condition |
ensures |
private LocationVariable |
heap |
private int |
id |
static java.lang.String |
INV_TACLET |
private Term |
mby |
private java.lang.String |
name |
static java.lang.String |
OP_EXC_TACLET |
static java.lang.String |
OP_TACLET |
private static java.lang.String |
OPTION |
private Contract.OriginalVariables |
origVars |
private Term |
represents |
private WellDefinednessCheck.Condition |
requires |
private IObserverFunction |
target |
(package private) TermBuilder |
TB |
private WellDefinednessCheck.Type |
type |
INVALID_ID
Constructor and Description |
---|
WellDefinednessCheck(java.lang.String name,
int id,
IObserverFunction target,
Contract.OriginalVariables origVars,
WellDefinednessCheck.Type type,
Services services) |
WellDefinednessCheck(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 represents,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
(package private) void |
addEnsures(Term ens) |
(package private) void |
addEnsures(WellDefinednessCheck.Condition ens) |
WellDefinednessCheck |
addRepresents(Term rep) |
(package private) void |
addRequires(Term req) |
(package private) void |
addRequires(WellDefinednessCheck.Condition req) |
private Term |
appendFreePre(Term pre,
ParsableVariable self,
ParsableVariable heap,
TermServices services)
Non-helper constructor methods cannot assume the free precondition, but
establish it.
|
private WellDefinednessCheck.TermListAndFunc |
buildFreePre(Term implicitPre,
ParsableVariable self,
ParsableVariable heap,
ImmutableList<ParsableVariable> params,
boolean taclet,
Services services)
Builds the "general assumption"
|
WellDefinednessCheck |
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.
|
(package private) void |
combineAccessible(Term acc,
Term accPre,
TermServices services) |
(package private) void |
combineAssignable(Term ass1,
Term ass2,
TermServices services) |
(package private) static RewriteTaclet |
createExcTaclet(java.lang.String name,
Term callTerm,
TermServices services)
Creates new well-definedness taclet for a pure method invocation, which can
potentially throw an exception.
|
WellDefinednessCheck.POTerms |
createPOTerms()
collects terms for precondition,
assignable clause and other specification elements,
and postcondition & signals-clause
|
ContractPO |
createProofObl(InitConfig initConfig)
Returns a proof obligation to the passed initConfig.
|
ProofOblInput |
createProofObl(InitConfig initConfig,
Contract contract)
Returns a proof obligation to the passed contract and initConfig.
|
ProofOblInput |
createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel)
Returns a proof obligation to the passed contract and initConfig.
|
(package private) static RewriteTaclet |
createTaclet(java.lang.String name,
Term callee,
Term callTerm,
Term pre,
boolean isStatic,
TermServices services)
Creates new well-definedness taclet for either an invariant reference or a pure
method invocation.
|
(package private) static RewriteTaclet |
createTaclet(java.lang.String name,
Term find1,
Term find2,
Term goal1,
Term goal2,
TermServices services)
Conjoins two well-definedness taclets for pure method invocations
|
boolean |
equals(java.lang.Object o) |
(package private) abstract Function |
generateMbyAtPreFunc(Services services) |
private Term |
generateParamsOK(ImmutableList<ParsableVariable> paramVars)
Generates the general assumption that all parameter arguments are valid.
|
private Term |
generateSelfCreated(ParsableVariable selfVar,
ParsableVariable heap)
Generates the general assumption that self is created.
|
private Term |
generateSelfExactType(ParsableVariable selfVar)
Generates the general assumption which defines the type of self.
|
private Term |
generateSelfNotNull(ParsableVariable selfVar)
Generates the general assumption that self is not null.
|
Term |
getAccessible() |
Term |
getAccessible(ProgramVariable heap) |
Term |
getAssignable() |
Term |
getAssignable(LocationVariable heap) |
abstract Term |
getAxiom()
Only for contracts with model_behaviour, the result is different from null.
|
abstract java.lang.String |
getBehaviour()
Detects the specification element's behaviour
|
Term |
getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
java.lang.String |
getDisplayName()
Returns the displayed name.
|
WellDefinednessCheck.Condition |
getEnsures() |
Term |
getEnsures(LocationVariable heap) |
Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Deprecated.
|
LocationVariable |
getHeap() |
private ImmutableList<LocationVariable> |
getHeaps() |
java.lang.String |
getHTMLText(Services services)
Returns the contract in pretty HTML format.
|
Term |
getMby() |
Term |
getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original ProgramVariables to replace them easier.
|
java.lang.String |
getPlainText(Services services)
Returns the contract in pretty plain text format.
|
Term |
getPost(WellDefinednessCheck.Condition post,
ParsableVariable result,
TermServices services)
Gets the full valid post-condition
|
Term |
getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
Term |
getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Deprecated.
|
Term |
getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Deprecated.
|
WellDefinednessCheck.TermAndFunc |
getPre(WellDefinednessCheck.Condition pre,
ParsableVariable self,
ParsableVariable heap,
ImmutableList<? extends ParsableVariable> parameters,
boolean taclet,
Services services)
Gets the full valid precondition, which holds in the element's pre-state.
|
ProofOblInput |
getProofObl(Services services)
Lookup the proof obligation belonging to the contract in the specification repository.
|
private static java.util.Map<ProgramVariable,ProgramVariable> |
getReplaceMap(ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> paramVars,
Contract.OriginalVariables vars,
ImmutableList<LocationVariable> heaps) |
Term |
getRepresents() |
WellDefinednessCheck.Condition |
getRequires() |
Term |
getRequires(LocationVariable heap) |
(package private) ImmutableList<Term> |
getRest()
Collects all remaining (implicitly or explicity) specified clauses
(except for pre-condition, post-condition and assignable-clause).
|
private static java.util.Map<ProgramVariable,SchemaVariable> |
getSchemaMap(SchemaVariable selfVar,
SchemaVariable resultVar,
SchemaVariable excVar,
java.util.Map<LocationVariable,SchemaVariable> atPreVars,
ImmutableList<ParsableVariable> paramVars,
Contract.OriginalVariables vars,
ImmutableList<LocationVariable> heaps) |
IObserverFunction |
getTarget()
Returns the contracted function symbol.
|
private java.lang.String |
getText(boolean includeHtmlMarkup,
Services services)
Return String to display contract in proof management dialog
|
Term |
getUpdates(Term mod,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
TermServices services)
Gets the necessary updates applicable to the post-condition
|
int |
hashCode() |
boolean |
hasMby()
Tells whether the contract contains a measured_by clause.
|
boolean |
hasSelfVar()
Checks if a self variable is originally provided.
|
int |
id()
Returns the id number of the contract.
|
boolean |
isConstructor() |
static boolean |
isOn()
This method checks, if well-definedness checks are generally turned on or off.
|
abstract boolean |
modelField()
Detects if the specification element is a true (i.e. not an invariant) model field
|
Name |
name() |
java.lang.String |
proofToString(Services services)
Returns a parseable String representation of the contract.
|
private ImmutableList<Term> |
replace(java.lang.Iterable<Term> l,
WellDefinednessPO.Variables vars) |
(package private) Term |
replace(Term t,
Contract.OriginalVariables newVars) |
private Term |
replace(Term t,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> paramVars,
Contract.OriginalVariables origVars,
ImmutableList<LocationVariable> heaps) |
Term |
replace(Term t,
WellDefinednessPO.Variables vars) |
private WellDefinednessCheck.Condition |
replace(WellDefinednessCheck.Condition pre,
Contract.OriginalVariables newVars) |
private WellDefinednessCheck.Condition |
replace(WellDefinednessCheck.Condition pre,
WellDefinednessPO.Variables vars) |
WellDefinednessCheck.POTerms |
replace(WellDefinednessCheck.POTerms po,
WellDefinednessPO.Variables vars) |
private Term |
replaceSV(Term t,
SchemaVariable self,
ImmutableList<ParsableVariable> params) |
private Term |
replaceSV(Term t,
SchemaVariable selfVar,
SchemaVariable resultVar,
SchemaVariable excVar,
java.util.Map<LocationVariable,SchemaVariable> atPreVars,
ImmutableList<ParsableVariable> paramVars,
Contract.OriginalVariables origVars,
ImmutableList<LocationVariable> heaps) |
(package private) WellDefinednessCheck.Condition |
replaceSV(WellDefinednessCheck.Condition pre,
SchemaVariable self,
ImmutableList<ParsableVariable> params) |
(package private) void |
setAccessible(Term acc) |
(package private) void |
setAssignable(Term ass,
TermServices services) |
(package private) void |
setEnsures(Term ens) |
(package private) void |
setMby(Term mby) |
(package private) void |
setRequires(Term req) |
private Pair<ImmutableList<Term>,ImmutableList<Term>> |
sort(Term spec)
Splits and sorts a (specification) term in such a way that implicit parts are in the
first and explicit parts in the second list.
|
private WellDefinednessCheck.Condition |
split(Term spec)
Splits a (specification) term into implicit and explicit parts (i.e. as written
in the specification) and reforms the conjunction in a sorted way, where implicit
parts appear first, and also labeled with the short-circuit term label.
|
boolean |
toBeSaved()
Tells whether, on saving a proof where this contract is available, the contract should be
saved too.
|
java.lang.String |
toString() |
(package private) WellDefinednessCheck.Type |
type() |
private java.lang.String |
typeString() |
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getGlobalDefs, getTypeName, isAuxiliary, setID, setTarget, transactionApplicableContract
getKJT, getVisibility
private static final java.lang.String OPTION
public static final java.lang.String INV_TACLET
public static final java.lang.String OP_TACLET
public static final java.lang.String OP_EXC_TACLET
private final java.lang.String name
private final int id
private final WellDefinednessCheck.Type type
private IObserverFunction target
private final LocationVariable heap
private final Contract.OriginalVariables origVars
private WellDefinednessCheck.Condition requires
private Term assignable
private WellDefinednessCheck.Condition ensures
private Term accessible
private Term mby
private Term represents
final TermBuilder TB
WellDefinednessCheck(java.lang.String name, int id, IObserverFunction target, Contract.OriginalVariables origVars, WellDefinednessCheck.Type type, Services services)
WellDefinednessCheck(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 represents, TermBuilder tb)
private Pair<ImmutableList<Term>,ImmutableList<Term>> sort(Term spec)
spec
- specification termprivate Term replaceSV(Term t, SchemaVariable self, ImmutableList<ParsableVariable> params)
private Term replaceSV(Term t, SchemaVariable selfVar, SchemaVariable resultVar, SchemaVariable excVar, java.util.Map<LocationVariable,SchemaVariable> atPreVars, ImmutableList<ParsableVariable> paramVars, Contract.OriginalVariables origVars, ImmutableList<LocationVariable> heaps)
private Term replace(Term t, ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,ProgramVariable> atPreVars, ImmutableList<ProgramVariable> paramVars, Contract.OriginalVariables origVars, ImmutableList<LocationVariable> heaps)
private static java.util.Map<ProgramVariable,SchemaVariable> getSchemaMap(SchemaVariable selfVar, SchemaVariable resultVar, SchemaVariable excVar, java.util.Map<LocationVariable,SchemaVariable> atPreVars, ImmutableList<ParsableVariable> paramVars, Contract.OriginalVariables vars, ImmutableList<LocationVariable> heaps)
private static java.util.Map<ProgramVariable,ProgramVariable> getReplaceMap(ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,ProgramVariable> atPreVars, ImmutableList<ProgramVariable> paramVars, Contract.OriginalVariables vars, ImmutableList<LocationVariable> heaps)
private WellDefinednessCheck.Condition split(Term spec)
spec
- specification termprivate WellDefinednessCheck.Condition replace(WellDefinednessCheck.Condition pre, Contract.OriginalVariables newVars)
private WellDefinednessCheck.Condition replace(WellDefinednessCheck.Condition pre, WellDefinednessPO.Variables vars)
private ImmutableList<Term> replace(java.lang.Iterable<Term> l, WellDefinednessPO.Variables vars)
private ImmutableList<LocationVariable> getHeaps()
private java.lang.String typeString()
private java.lang.String getText(boolean includeHtmlMarkup, Services services)
includeHtmlMarkup
- services
- private Term appendFreePre(Term pre, ParsableVariable self, ParsableVariable heap, TermServices services)
pre
- specified preconditionself
- self variableheap
- heap variableservices
- private Term generateSelfNotNull(ParsableVariable selfVar)
pm
- The IProgramMethod
to execute.selfVar
- The self variable.private Term generateSelfCreated(ParsableVariable selfVar, ParsableVariable heap)
pm
- The IProgramMethod
to execute.selfVar
- The self variable.private Term generateSelfExactType(ParsableVariable selfVar)
pm
- The IProgramMethod
to execute.selfVar
- The self variable.selfKJT
- The KeYJavaType
of the self variable.private Term generateParamsOK(ImmutableList<ParsableVariable> paramVars)
paramVars
- The parameters ProgramVariable
s.private WellDefinednessCheck.TermListAndFunc buildFreePre(Term implicitPre, ParsableVariable self, ParsableVariable heap, ImmutableList<ParsableVariable> params, boolean taclet, Services services)
implicitPre
- the implicit preconditionself
- self variableheap
- heap variableparams
- list of parameter variablestaclet
- boolean is true if used for a wd-tacletservices
- Term
containing the general assumptions.static final RewriteTaclet createTaclet(java.lang.String name, Term find1, Term find2, Term goal1, Term goal2, TermServices services)
name
- taclet namefind1
- first find termfind2
- second find termgoal1
- first preconditiongoal2
- second preconditionservices
- static final RewriteTaclet createTaclet(java.lang.String name, Term callee, Term callTerm, Term pre, boolean isStatic, TermServices services)
name
- taclet namecallee
- the receiver variable as a termcallTerm
- the whole invocation termpre
- the method's or invariant's preconditionisStatic
- a boolean to tell if the method is staticservices
- static final RewriteTaclet createExcTaclet(java.lang.String name, Term callTerm, TermServices services)
name
- taclet namecallTerm
- the whole invocation termservices
- final Term replace(Term t, Contract.OriginalVariables newVars)
final WellDefinednessCheck.Condition replaceSV(WellDefinednessCheck.Condition pre, SchemaVariable self, ImmutableList<ParsableVariable> params)
final void setMby(Term mby)
final void addRequires(WellDefinednessCheck.Condition req)
final void addRequires(Term req)
final void setRequires(Term req)
final void setAssignable(Term ass, TermServices services)
final void combineAssignable(Term ass1, Term ass2, TermServices services)
final void setAccessible(Term acc)
final void combineAccessible(Term acc, Term accPre, TermServices services)
final void addEnsures(WellDefinednessCheck.Condition ens)
final void addEnsures(Term ens)
final void setEnsures(Term ens)
final WellDefinednessCheck.Type type()
ImmutableList<Term> getRest()
public abstract java.lang.String getBehaviour()
public abstract boolean modelField()
public abstract Term getAxiom()
public WellDefinednessCheck combine(WellDefinednessCheck wdc, TermServices services)
wdc
- the well-definedness check to be combined with the current oneservices
- public static final boolean isOn()
public final WellDefinednessCheck.POTerms createPOTerms()
public final WellDefinednessCheck addRepresents(Term rep)
public final WellDefinednessCheck.TermAndFunc getPre(WellDefinednessCheck.Condition pre, ParsableVariable self, ParsableVariable heap, ImmutableList<? extends ParsableVariable> parameters, boolean taclet, Services services)
pre
- the precondition with the original variablesself
- the new self variableheap
- the new heap variableparameters
- the new parameter listtaclet
- is true if the precondition will be used in a tacletservices
- public final Term getPost(WellDefinednessCheck.Condition post, ParsableVariable result, TermServices services)
post
- post-condition with original variablesresult
- the new result variableservices
- public final Term getUpdates(Term mod, LocationVariable heap, ProgramVariable heapAtPre, Term anonHeap, TermServices services)
mod
- the assignable-clauseheap
- the current heap variableheapAtPre
- the current variable for the heap of the pre-stateanonHeap
- the anonymous heap termservices
- public final Term replace(Term t, WellDefinednessPO.Variables vars)
public final WellDefinednessCheck.POTerms replace(WellDefinednessCheck.POTerms po, WellDefinednessPO.Variables vars)
public final LocationVariable getHeap()
public final Name name()
public final WellDefinednessCheck.Condition getRequires()
public final Term getAssignable()
public final Term getAccessible()
public final WellDefinednessCheck.Condition getEnsures()
public final Term getEnsures(LocationVariable heap)
public final Term getRepresents()
public final boolean isConstructor()
public final java.lang.String toString()
toString
in class java.lang.Object
public final java.lang.String getName()
SpecificationElement
getName
in interface SpecificationElement
public final int id()
Contract
public final boolean hasMby()
Contract
public final Term getRequires(LocationVariable heap)
getRequires
in interface Contract
public final Term getAssignable(LocationVariable heap)
getAssignable
in interface Contract
public final Term getAccessible(ProgramVariable heap)
getAccessible
in interface Contract
public final java.lang.String getHTMLText(Services services)
Contract
getHTMLText
in interface Contract
services
- services instancepublic final java.lang.String getPlainText(Services services)
Contract
getPlainText
in interface Contract
services
- services instancepublic final java.lang.String proofToString(Services services)
Contract
proofToString
in interface Contract
services
- the services instancepublic final IObserverFunction getTarget()
Contract
public final ProofOblInput createProofObl(InitConfig initConfig, Contract contract)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationcontract
- the contractpublic final ProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean addSymbolicExecutionLabel)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationcontract
- the contractaddSymbolicExecutionLabel
- boolean saying whether symbolic execution api is supportedpublic final ContractPO createProofObl(InitConfig initConfig)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationpublic final ProofOblInput getProofObl(Services services)
Contract
getProofObl
in interface Contract
services
- the services instancepublic final java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public final boolean toBeSaved()
Contract
public final boolean hasSelfVar()
Contract
hasSelfVar
in interface Contract
true
self variable is originally provided, false
no self variable
available.public final Contract.OriginalVariables getOrigVars()
Contract
getOrigVars
in interface Contract
public final boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public final int hashCode()
hashCode
in class java.lang.Object
@Deprecated public final Term getPre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services) throws java.lang.UnsupportedOperationException
Contract
@Deprecated public final Term getPre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services) throws java.lang.UnsupportedOperationException
Contract
@Deprecated public final Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services) throws java.lang.UnsupportedOperationException
Contract
@Deprecated public final Term getPre(java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services) throws java.lang.UnsupportedOperationException
Contract
getPre
in interface Contract
heapContext
- heap contextheapTerms
- heap termsselfTerm
- term of self variableparamTerms
- terms of parameter variablesatPres
- terms of variables at previous heapservices
- services objectjava.lang.UnsupportedOperationException
@Deprecated public final Term getDep(LocationVariable heap, boolean atPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
@Deprecated public final Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
Contract
getDep
in interface Contract
heap
- the heap variableatPre
- boolean whether old heap should be usedheapTerm
- the heap variable termselfTerm
- term of self variableparamTerms
- terms of parameter variablesatPres
- terms of variables at previous heapservices
- services object@Deprecated public final Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
getGlobalDefs
in interface Contract
@Deprecated public final Term getMby(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services) throws java.lang.UnsupportedOperationException
Contract
@Deprecated public final Term getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services) throws java.lang.UnsupportedOperationException
Contract
getMby
in interface Contract
heapTerms
- terms for the heap contextselfTerm
- term of self variableparamTerms
- terms of parameter variablesatPres
- terms of variables at previous heapservices
- services objectjava.lang.UnsupportedOperationException