public final class InitiallyClauseImpl extends java.lang.Object implements InitiallyClause
Constructor and Description |
---|
InitiallyClauseImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term inv,
ParsableVariable selfVar,
LabeledParserRuleContext originalSpec)
Creates a class invariant.
|
Modifier and Type | Method and Description |
---|---|
Term |
getClause(ParsableVariable selfVar,
TermServices services)
Returns the formula without implicit all-quantification over
the receiver object.
|
java.lang.String |
getDisplayName()
Returns the displayed name.
|
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.
|
LabeledParserRuleContext |
getOriginalSpec() |
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
InitiallyClause |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
InitiallyClause |
setKJT(KeYJavaType newKjt) |
java.lang.String |
toString() |
public InitiallyClauseImpl(java.lang.String name, java.lang.String displayName, KeYJavaType kjt, VisibilityModifier visibility, Term inv, ParsableVariable selfVar, LabeledParserRuleContext originalSpec)
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 objectoriginalSpec
- public InitiallyClause map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface InitiallyClause
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 getClause(ParsableVariable selfVar, TermServices services)
InitiallyClause
getClause
in interface InitiallyClause
public LabeledParserRuleContext getOriginalSpec()
getOriginalSpec
in interface InitiallyClause
public VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
public java.lang.String toString()
toString
in class java.lang.Object
public InitiallyClause setKJT(KeYJavaType newKjt)
setKJT
in interface InitiallyClause
Copyright © 2003-2019 The KeY-Project.