public final class ContractAxiom extends ClassAxiom
Modifier and Type | Field and Description |
---|---|
private java.util.Map<LocationVariable,ProgramVariable> |
atPreVars |
private KeYJavaType |
kjt |
private java.lang.String |
name |
private Term |
originalMby |
private ImmutableList<ProgramVariable> |
originalParamVars |
private Term |
originalPost |
private Term |
originalPre |
private ProgramVariable |
originalResultVar |
private ProgramVariable |
originalSelfVar |
private IObserverFunction |
target |
private VisibilityModifier |
visibility |
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() |
getDisplayName
private final java.lang.String name
private final IObserverFunction target
private final KeYJavaType kjt
private final VisibilityModifier visibility
private final Term originalPre
private final Term originalPost
private final Term originalMby
private final ProgramVariable originalSelfVar
private final ProgramVariable originalResultVar
private final ImmutableList<ProgramVariable> originalParamVars
private final java.util.Map<LocationVariable,ProgramVariable> atPreVars
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 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