de.uka.ilkd.key.speclang.jml.pretranslation

Class TextualJMLConstruct

java.lang.Object

de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct

Direct Known Subclasses:

TextualJMLClassAxiom, TextualJMLClassInv, TextualJMLDepends, TextualJMLFieldDecl, TextualJMLInitially, TextualJMLLoopSpec, TextualJMLMergePointDecl, TextualJMLMethodDecl, TextualJMLRepresents, TextualJMLSetStatement, TextualJMLSpecCase

public abstract class TextualJMLConstruct
extends java.lang.Object

Objects of this type represent the various JML specification constructs in textual, unprocessed form.

Field Summary

Fields

Modifier and Type	Field and Description
private Position	approxPos
private boolean	loopContract
protected ImmutableList<java.lang.String>	mods
protected java.lang.String	name A user-provided identifier to keep an overview over large specification collections
private java.lang.String	sourceFile

Constructor Summary

Constructors

Constructor and Description
TextualJMLConstruct(ImmutableList<java.lang.String> mods)
TextualJMLConstruct(ImmutableList<java.lang.String> mods, java.lang.String name)

Method Summary

Modifier and Type	Method and Description
protected void	addGeneric(java.util.Map<java.lang.String,ImmutableList<PositionedString>> item, PositionedString ps)
Position	getApproxPosition() Return the approximate position of this construct.
ImmutableList<java.lang.String>	getMods()
java.lang.String	getSourceFileName() Return the source file name where this construct appears.
boolean	isLoopContract()
(package private) void	setLoopContract(boolean loopContract)
protected void	setPosition(PositionedString ps) Sets the approximate position of this construct when first called with a valid position.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

mods

protected final ImmutableList<java.lang.String> mods

approxPos

private Position approxPos

sourceFile

private java.lang.String sourceFile

loopContract

private boolean loopContract

name

protected java.lang.String name

A user-provided identifier to keep an overview over large specification collections

Constructor Detail

TextualJMLConstruct

public TextualJMLConstruct(ImmutableList<java.lang.String> mods)

TextualJMLConstruct

public TextualJMLConstruct(ImmutableList<java.lang.String> mods,
                           java.lang.String name)

Method Detail

isLoopContract

public final boolean isLoopContract()

Returns:

true if and only if this is a loop contract.

See Also:

LoopContract

setLoopContract

final void setLoopContract(boolean loopContract)

Parameters:

loopContract - boolean to identify contract as loop contract

See Also:

isLoopContract()

getMods

public final ImmutableList<java.lang.String> getMods()

getApproxPosition

public Position getApproxPosition()

Return the approximate position of this construct. This is usually the position of the specification line parsed first. Implementations can set it using setPosition or addGeneric.

getSourceFileName

public java.lang.String getSourceFileName()

Return the source file name where this construct appears.

setPosition

protected void setPosition(PositionedString ps)

Sets the approximate position of this construct when first called with a valid position. The approximate position can still be changed while it is undefined. Also set source file name if known.

Parameters:

ps - set position of the construct

addGeneric

protected void addGeneric(java.util.Map<java.lang.String,ImmutableList<PositionedString>> item,
                          PositionedString ps)