public final class ModelMethodExecution extends ClassAxiom
displayName
Constructor and Description |
---|
ModelMethodExecution(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility) |
ModelMethodExecution(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility) |
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object o) |
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
ImmutableSet<Taclet> |
getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services)
The axiom as one or many taclets, where the non-defining occurrences of
the passed observers are replaced by their "limited" counterparts.
|
IObserverFunction |
getTarget()
Returns the axiomatised function symbol.
|
ImmutableSet<Pair<Sort,IObserverFunction>> |
getUsedObservers(Services services)
Returns the pairs (kjt, obs) for which there is an occurrence of
o.obs in the axiom, where kjt is the type of o (excluding the
defining occurrence of the axiom target).
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
int |
hashCode() |
ModelMethodExecution |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
getDisplayName
public ModelMethodExecution(java.lang.String name, IObserverFunction target, KeYJavaType kjt, VisibilityModifier visibility)
public ModelMethodExecution(java.lang.String name, java.lang.String displayName, IObserverFunction target, KeYJavaType kjt, VisibilityModifier visibility)
public ModelMethodExecution map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
op
- the operator to apply.services
- services.public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public ImmutableSet<Taclet> getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit, Services services)
ClassAxiom
getTaclets
in class ClassAxiom
public ImmutableSet<Pair<Sort,IObserverFunction>> getUsedObservers(Services services)
ClassAxiom
getUsedObservers
in class ClassAxiom
public java.lang.String getName()
SpecificationElement
public IObserverFunction getTarget()
ClassAxiom
getTarget
in class ClassAxiom
public KeYJavaType getKJT()
SpecificationElement
public VisibilityModifier getVisibility()
SpecificationElement
Copyright © 2003-2019 The KeY-Project.