de.uka.ilkd.key.speclang

Class PartialInvAxiom

java.lang.Object

de.uka.ilkd.key.speclang.ClassAxiom

de.uka.ilkd.key.speclang.PartialInvAxiom

All Implemented Interfaces:

SpecificationElement

public final class PartialInvAxiom
extends ClassAxiom

A class axiom which is essentially of the form "o. -> phi": it demands that the invariants of the objects of a particular class imply a particular formula. These axioms are logically weaker than the full definitions of expressed as RepresentsAxioms, but they may have higher visibility, making them available in proofs where the corresponding full definition is not.

Field Summary

Fields

Modifier and Type	Field and Description
private ClassInvariant	inv
private IObserverFunction	target

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

displayName

Constructor Summary

Constructors

Constructor and Description
PartialInvAxiom(ClassInvariant inv, boolean isStatic, Services services) Creates a new class axiom.
PartialInvAxiom(ClassInvariant inv, java.lang.String displayName, Services services)

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object o)
ClassInvariant	getInv()
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()
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

inv

private final ClassInvariant inv

target

private final IObserverFunction target

Constructor Detail

PartialInvAxiom

public PartialInvAxiom(ClassInvariant inv,
                       boolean isStatic,
                       Services services)

Creates a new class axiom.

Parameters:

inv - (partial) invariant from which the axiom is derived

isStatic - whether the axiom should match static invariants (i.e., <$inv>) or instance invariants (i.e., <inv>)

services -

PartialInvAxiom

public PartialInvAxiom(ClassInvariant inv,
                       java.lang.String displayName,
                       Services services)

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

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

getInv

public ClassInvariant getInv()