public final class RepresentsAxiom extends ClassAxiom
displayName
Constructor and Description |
---|
RepresentsAxiom(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term rep,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars) |
RepresentsAxiom(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term rep,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars) |
Modifier and Type | Method and Description |
---|---|
RepresentsAxiom |
conjoin(RepresentsAxiom ax,
TermBuilder tb)
Conjoins two represents clauses with minimum visibility.
|
boolean |
equals(java.lang.Object o) |
Term |
getAxiom(ParsableVariable heapVar,
ParsableVariable selfVar,
Services services) |
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.
|
Contract.OriginalVariables |
getOrigVars() |
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() |
SpecificationElement |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
RepresentsAxiom |
setKJT(KeYJavaType newKjt) |
java.lang.String |
toString() |
getDisplayName
public RepresentsAxiom(java.lang.String name, IObserverFunction target, KeYJavaType kjt, VisibilityModifier visibility, Term pre, Term rep, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,ProgramVariable> atPreVars)
public RepresentsAxiom(java.lang.String name, java.lang.String displayName, IObserverFunction target, KeYJavaType kjt, VisibilityModifier visibility, Term pre, Term rep, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,ProgramVariable> atPreVars)
public SpecificationElement 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 Term getAxiom(ParsableVariable heapVar, ParsableVariable selfVar, Services services)
public java.lang.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 java.lang.String toString()
toString
in class java.lang.Object
public RepresentsAxiom setKJT(KeYJavaType newKjt)
public RepresentsAxiom conjoin(RepresentsAxiom ax, TermBuilder tb)
Conjoins two represents clauses with minimum visibility. An exception is thrown if the targets or types are different.
Known issue: public clauses in subclasses are hidden by protected clauses in superclasses; this only applies to observers outside the package of the subclass (whenever package-privacy is implemented).
ax
- some represents clause.tb
- a term builder.ax
.public Contract.OriginalVariables getOrigVars()
Copyright © 2003-2019 The KeY-Project.