de.uka.ilkd.key.speclang

Class ClassAxiom

java.lang.Object

de.uka.ilkd.key.speclang.ClassAxiom

All Implemented Interfaces:

SpecificationElement

Direct Known Subclasses:

ClassAxiomImpl, ContractAxiom, ModelMethodExecution, PartialInvAxiom, QueryAxiom, RepresentsAxiom

public abstract class ClassAxiom
extends java.lang.Object
implements SpecificationElement

An axiom originating from a (JML) specification, belonging to a particular class, and constraining a particular observer symbol. A class axiom always has an associated visibility. The visibility determines in which proofs the axiom is available, in accordance with the visibility rules of Java. If visible, it is made available not as a formula, but as one or many taclets (for performance reasons).

Field Summary

Fields

Modifier and Type	Field and Description
protected java.lang.String	displayName

Constructor Summary

Constructors

Constructor and Description
ClassAxiom()

Method Summary

Modifier and Type	Method and Description
java.lang.String	getDisplayName() Returns the displayed name.
abstract 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.
abstract IObserverFunction	getTarget() Returns the axiomatised function symbol.
abstract 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).

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.speclang.SpecificationElement

getKJT, getName, getVisibility

Field Detail

displayName

protected java.lang.String displayName

Constructor Detail

ClassAxiom

public ClassAxiom()

Method Detail

getTarget

public abstract IObserverFunction getTarget()

Returns the axiomatised function symbol.

getUsedObservers

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

getTaclets

public abstract 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.

getDisplayName

public java.lang.String getDisplayName()

Description copied from interface: SpecificationElement

Returns the displayed name.

Specified by:

getDisplayName in interface SpecificationElement