public final class ContractAxiom extends ClassAxiom
displayName
Constructor and Description |
---|
ContractAxiom(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term post,
Term mby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
ContractAxiom(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term originalPre,
Term originalPost,
Term originalMby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
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() |
ContractAxiom |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
getDisplayName
public ContractAxiom(java.lang.String name, IObserverFunction target, KeYJavaType kjt, VisibilityModifier visibility, Term pre, Term post, Term mby, java.util.Map<LocationVariable,ProgramVariable> atPreVars, ProgramVariable selfVar, ProgramVariable resultVar, ImmutableList<ProgramVariable> paramVars)
public ContractAxiom(java.lang.String name, java.lang.String displayName, IObserverFunction target, KeYJavaType kjt, VisibilityModifier visibility, Term originalPre, Term originalPost, Term originalMby, java.util.Map<LocationVariable,ProgramVariable> atPreVars, ProgramVariable selfVar, ProgramVariable resultVar, ImmutableList<ProgramVariable> paramVars)
public ContractAxiom map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
op
- the operator to apply.services
- services.public ImmutableSet<Taclet> getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit, Services services)
ClassAxiom
getTaclets
in class ClassAxiom
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
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.