public final class ClassInvariantImpl extends java.lang.Object implements ClassInvariant
Constructor and Description |
---|
ClassInvariantImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term inv,
ParsableVariable selfVar)
Creates a class invariant.
|
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.
|
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 |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
ClassInvariant |
setKJT(KeYJavaType newKjt)
Returns another class invariant like this one, except that it refers to the
passed KeYJavaType.
|
java.lang.String |
toString() |
public ClassInvariantImpl(java.lang.String name, java.lang.String displayName, KeYJavaType kjt, VisibilityModifier visibility, Term inv, ParsableVariable selfVar)
name
- the unique internal name of the invariantdisplayName
- the displayed name of the invariantkjt
- the KeYJavaType to which the invariant belongsvisibility
- the visibility of the invariant
(null for default visibility)inv
- the invariant formula itselfselfVar
- the variable used for the receiver objectpublic ClassInvariant map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface ClassInvariant
map
in interface SpecificationElement
op
- the operator to apply.services
- services.public java.lang.String getName()
SpecificationElement
getName
in interface SpecificationElement
public java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
public Term getInv(ParsableVariable selfVar, TermServices services)
ClassInvariant
getInv
in interface ClassInvariant
public Term getOriginalInv()
ClassInvariant
getOriginalInv
in interface ClassInvariant
public boolean isStatic()
ClassInvariant
isStatic
in interface ClassInvariant
public VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
public ClassInvariant setKJT(KeYJavaType newKjt)
ClassInvariant
setKJT
in interface ClassInvariant
public java.lang.String toString()
toString
in class java.lang.Object
public Contract.OriginalVariables getOrigVars()
ClassInvariant
getOrigVars
in interface ClassInvariant
Copyright © 2003-2019 The KeY-Project.