public interface ClassInvariant extends SpecificationElement
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 |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
ClassInvariant |
setKJT(KeYJavaType kjt)
Returns another class invariant like this one, except that it refers to the
passed KeYJavaType.
|
getDisplayName, getKJT, getName, getVisibility
Term getInv(ParsableVariable selfVar, TermServices services)
Term getOriginalInv()
boolean isStatic()
ClassInvariant setKJT(KeYJavaType kjt)
Contract.OriginalVariables getOrigVars()
ClassInvariant map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface SpecificationElement
op
- the operator to apply.services
- services.Copyright © 2003-2019 The KeY-Project.