public final class ClassAxiomImpl extends ClassAxiom
displayName
Constructor and Description |
---|
ClassAxiomImpl(java.lang.String name,
KeYJavaType kjt,
VisibilityModifier visibility,
Term rep,
ProgramVariable selfVar) |
ClassAxiomImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term rep,
ProgramVariable selfVar) |
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()
Class axioms do not have targets (in opposition to represents clauses)
|
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() |
ClassAxiomImpl |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
java.lang.String |
toString() |
getDisplayName
public ClassAxiomImpl(java.lang.String name, KeYJavaType kjt, VisibilityModifier visibility, Term rep, ProgramVariable selfVar)
public ClassAxiomImpl(java.lang.String name, java.lang.String displayName, KeYJavaType kjt, VisibilityModifier visibility, Term rep, ProgramVariable selfVar)
public ClassAxiomImpl 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 java.lang.String getName()
SpecificationElement
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 java.lang.String toString()
toString
in class java.lang.Object
public IObserverFunction getTarget()
getTarget
in class ClassAxiom
Copyright © 2003-2019 The KeY-Project.