de.uka.ilkd.key.speclang

Class ClassInvariantImpl

java.lang.Object

de.uka.ilkd.key.speclang.ClassInvariantImpl

All Implemented Interfaces:

ClassInvariant, SpecificationElement

public final class ClassInvariantImpl
extends java.lang.Object
implements ClassInvariant

Standard implementation of the ClassInvariant interface.

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	displayName
private boolean	isStatic
private KeYJavaType	kjt
private java.lang.String	name
private Term	originalInv
private ParsableVariable	originalSelfVar
private VisibilityModifier	visibility

Constructor Summary

Constructors

Constructor and Description
ClassInvariantImpl(java.lang.String name, java.lang.String displayName, KeYJavaType kjt, VisibilityModifier visibility, Term inv, ParsableVariable selfVar) Creates a class invariant.

Method Summary

Modifier and Type	Method and Description
java.lang.String	getDisplayName() Returns the displayed name.
Term	getInv(ParsableVariable selfVar, TermServices services) Returns the invariant formula without implicit all-quantification over the receiver object.
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.
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.
private java.util.Map<Operator,Operator>	getReplaceMap(ParsableVariable selfVar, TermServices services)
VisibilityModifier	getVisibility() Returns the visibility of the invariant (null for default visibility)
boolean	isStatic() Tells whether the invariant is static (i.e., does not refer to a receiver object).
ClassInvariant	setKJT(KeYJavaType newKjt) Returns another class invariant like this one, except that it refers to the passed KeYJavaType.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

name

private final java.lang.String name

displayName

private final java.lang.String displayName

kjt

private final KeYJavaType kjt

visibility

private final VisibilityModifier visibility

originalInv

private final Term originalInv

originalSelfVar

private final ParsableVariable originalSelfVar

isStatic

private final boolean isStatic

Constructor Detail

ClassInvariantImpl

public ClassInvariantImpl(java.lang.String name,
                          java.lang.String displayName,
                          KeYJavaType kjt,
                          VisibilityModifier visibility,
                          Term inv,
                          ParsableVariable selfVar)

Creates a class invariant.

Parameters:

name - the unique internal name of the invariant

displayName - the displayed name of the invariant

kjt - the KeYJavaType to which the invariant belongs

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

inv - the invariant formula itself

selfVar - the variable used for the receiver object

Method Detail

getReplaceMap

private java.util.Map<Operator,Operator> getReplaceMap(ParsableVariable selfVar,
                                                       TermServices services)

getName

public java.lang.String getName()

Description copied from interface: SpecificationElement

Returns the unique internal name of the specification element.

Specified by:

getName in interface SpecificationElement

getDisplayName

public java.lang.String getDisplayName()

Description copied from interface: SpecificationElement

Returns the displayed name.

Specified by:

getDisplayName in interface SpecificationElement

getKJT

public KeYJavaType getKJT()

Description copied from interface: SpecificationElement

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

Specified by:

getKJT in interface SpecificationElement

getInv

public Term getInv(ParsableVariable selfVar,
                   TermServices services)

Description copied from interface: ClassInvariant

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

Specified by:

getInv in interface ClassInvariant

getOriginalInv

public Term getOriginalInv()

Description copied from interface: ClassInvariant

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

Specified by:

getOriginalInv in interface ClassInvariant

isStatic

public boolean isStatic()

Description copied from interface: ClassInvariant

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

Specified by:

isStatic in interface ClassInvariant

getVisibility

public VisibilityModifier getVisibility()

Description copied from interface: SpecificationElement

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

Specified by:

getVisibility in interface SpecificationElement

setKJT

public ClassInvariant setKJT(KeYJavaType newKjt)

Description copied from interface: ClassInvariant

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

Specified by:

setKJT in interface ClassInvariant

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getOrigVars

public Contract.OriginalVariables getOrigVars()

Description copied from interface: ClassInvariant

Returns the original Self Variable to replace it easier.

Specified by:

getOrigVars in interface ClassInvariant