public interface InitiallyClause extends SpecificationElement
Modifier and Type | Method and Description |
---|---|
Term |
getClause(ParsableVariable selfVar,
TermServices services)
Returns the formula without implicit all-quantification over
the receiver object.
|
LabeledParserRuleContext |
getOriginalSpec() |
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) |
getDisplayName, getKJT, getName, getVisibility
InitiallyClause map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface SpecificationElement
op
- the operator to apply.services
- services.Term getClause(ParsableVariable selfVar, TermServices services)
LabeledParserRuleContext getOriginalSpec()
InitiallyClause setKJT(KeYJavaType newKjt)
Copyright © 2003-2019 The KeY-Project.