public final class PartialInvAxiom extends ClassAxiom
Modifier and Type | Field and Description |
---|---|
private ClassInvariant |
inv |
private IObserverFunction |
target |
displayName
Constructor and Description |
---|
PartialInvAxiom(ClassInvariant inv,
boolean isStatic,
Services services)
Creates a new class axiom.
|
PartialInvAxiom(ClassInvariant inv,
String displayName,
Services services) |
Modifier and Type | Method and Description |
---|---|
boolean |
equals(Object o) |
ClassInvariant |
getInv() |
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
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() |
String |
toString() |
getDisplayName
private final ClassInvariant inv
private final IObserverFunction target
public PartialInvAxiom(ClassInvariant inv, boolean isStatic, Services services)
inv
- (partial) invariant from which the axiom is derivedisStatic
- whether the axiom should match static invariants (i.e., <$inv>) or instance invariants (i.e., <inv>)services
- public PartialInvAxiom(ClassInvariant inv, String displayName, Services services)
public String getName()
SpecificationElement
public IObserverFunction getTarget()
ClassAxiom
getTarget
in class ClassAxiom
public KeYJavaType getKJT()
SpecificationElement
public VisibilityModifier getVisibility()
SpecificationElement
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 ClassInvariant getInv()