de.uka.ilkd.key.speclang

Interface ClassInvariant

All Superinterfaces:

SpecificationElement

All Known Implementing Classes:

ClassInvariantImpl

public interface ClassInvariant
extends SpecificationElement

A class invariant. Objects of type ClassInvariant are an intermediate result of the specification language front ends; ultimately, they give rise to instances of the ClassAxiom class (more precisely, of its subclasses RepresentsAxiom and PartialInvAxiom), through which class invariants are actually used in proofs.

Method Summary

Modifier and Type	Method and Description
Term	getInv(ParsableVariable selfVar, TermServices services) Returns the invariant formula without implicit all-quantification over the receiver object.
Term	getOriginalInv() Returns the invariant formula without implicit all-quantification over the receiver object.
Contract.OriginalVariables	getOrigVars() Returns the original Self Variable to replace it easier.
boolean	isStatic() Tells whether the invariant is static (i.e., does not refer to a receiver object).
ClassInvariant	setKJT(KeYJavaType kjt) Returns another class invariant like this one, except that it refers to the passed KeYJavaType.

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

getDisplayName, getKJT, getName, getVisibility

Method Detail

getInv

Term getInv(ParsableVariable selfVar,
            TermServices services)

Returns the invariant formula without implicit all-quantification over the receiver object.

getOriginalInv

Term getOriginalInv()

Returns the invariant formula without implicit all-quantification over the receiver object.

isStatic

boolean isStatic()

Tells whether the invariant is static (i.e., does not refer to a receiver object).

setKJT

ClassInvariant setKJT(KeYJavaType kjt)

Returns another class invariant like this one, except that it refers to the passed KeYJavaType.

getOrigVars

Contract.OriginalVariables getOrigVars()

Returns the original Self Variable to replace it easier.