de.uka.ilkd.key.speclang

Interface InitiallyClause

All Superinterfaces:

SpecificationElement

All Known Implementing Classes:

InitiallyClauseImpl

public interface InitiallyClause
extends SpecificationElement

Method Summary

Modifier and Type	Method and Description
Term	getClause(ParsableVariable selfVar, TermServices services) Returns the formula without implicit all-quantification over the receiver object.
PositionedString	getOriginalSpec()
InitiallyClause	setKJT(KeYJavaType newKjt)

Methods inherited from interface de.uka.ilkd.key.speclang.SpecificationElement

getDisplayName, getKJT, getName, getVisibility

Method Detail

getClause

Term getClause(ParsableVariable selfVar,
               TermServices services)

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

getOriginalSpec

PositionedString getOriginalSpec()

setKJT

InitiallyClause setKJT(KeYJavaType newKjt)