de.uka.ilkd.key.speclang

Class RepresentsAxiom

java.lang.Object

de.uka.ilkd.key.speclang.ClassAxiom

de.uka.ilkd.key.speclang.RepresentsAxiom

All Implemented Interfaces:

SpecificationElement

public final class RepresentsAxiom
extends ClassAxiom

A class axiom corresponding to a JML* represents clause.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<LocationVariable,ProgramVariable>	atPreVars
private KeYJavaType	kjt
private java.lang.String	name
private ImmutableList<ProgramVariable>	originalParamVars
private Term	originalPre
private Term	originalRep
private ProgramVariable	originalSelfVar
private IObserverFunction	target
private VisibilityModifier	visibility

Fields inherited from class de.uka.ilkd.key.speclang.ClassAxiom

displayName

Constructor Summary

Constructors

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)

Method Summary

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()
private boolean	isFunctional(Services services)
RepresentsAxiom	setKJT(KeYJavaType newKjt)
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.speclang.ClassAxiom

getDisplayName

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

name

private final java.lang.String name

target

private final IObserverFunction target

kjt

private final KeYJavaType kjt

visibility

private final VisibilityModifier visibility

originalPre

private final Term originalPre

originalRep

private final Term originalRep

originalSelfVar

private final ProgramVariable originalSelfVar

atPreVars

private final java.util.Map<LocationVariable,ProgramVariable> atPreVars

originalParamVars

private final ImmutableList<ProgramVariable> originalParamVars

Constructor Detail

RepresentsAxiom

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)

RepresentsAxiom

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)

Method Detail

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

isFunctional

private boolean isFunctional(Services services)

getAxiom

public Term getAxiom(ParsableVariable heapVar,
                     ParsableVariable selfVar,
                     Services services)

getName

public java.lang.String getName()

Description copied from interface: SpecificationElement

Returns the unique internal name of the specification element.

getTarget

public IObserverFunction getTarget()

Description copied from class: ClassAxiom

Returns the axiomatised function symbol.

Specified by:

getTarget in class ClassAxiom

getKJT

public KeYJavaType getKJT()

Description copied from interface: SpecificationElement

Returns the KeYJavaType representing the class/interface to which the specification element belongs.

getVisibility

public VisibilityModifier getVisibility()

Description copied from interface: SpecificationElement

Returns the visibility of the invariant (null for default visibility)

getTaclets

public ImmutableSet<Taclet> getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
                                       Services services)

Description copied from class: ClassAxiom

The axiom as one or many taclets, where the non-defining occurrences of the passed observers are replaced by their "limited" counterparts.

Specified by:

getTaclets in class ClassAxiom

getUsedObservers

public ImmutableSet<Pair<Sort,IObserverFunction>> getUsedObservers(Services services)

Description copied from class: ClassAxiom

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).

Specified by:

getUsedObservers in class ClassAxiom

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

setKJT

public RepresentsAxiom setKJT(KeYJavaType newKjt)

conjoin

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).

Parameters:

tb - TODO

getOrigVars

public Contract.OriginalVariables getOrigVars()