public abstract class ClassAxiom extends java.lang.Object implements SpecificationElement
Modifier and Type | Field and Description |
---|---|
protected java.lang.String |
displayName |
Constructor and Description |
---|
ClassAxiom() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getDisplayName()
Returns the displayed name.
|
abstract 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.
|
abstract IObserverFunction |
getTarget()
Returns the axiomatised function symbol.
|
abstract 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).
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getKJT, getName, getVisibility
public abstract IObserverFunction getTarget()
public abstract ImmutableSet<Pair<Sort,IObserverFunction>> getUsedObservers(Services services)
public abstract ImmutableSet<Taclet> getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit, Services services)
public java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement