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

Class TextualJMLLoopSpec

java.lang.Object

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

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

public final class TextualJMLLoopSpec
extends TextualJMLConstruct

A JML loop specification (invariant, assignable clause, decreases clause, ...) in textual form.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<java.lang.String,ImmutableList<PositionedString>>	assignables
private java.util.Map<java.lang.String,ImmutableList<PositionedString>>	freeInvariants
private ImmutableList<PositionedString>	infFlowSpecs
private java.util.Map<java.lang.String,ImmutableList<PositionedString>>	invariants
private PositionedString	variant

Fields inherited from class de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct

mods, name

Constructor Summary

Constructors

Constructor and Description
TextualJMLLoopSpec(ImmutableList<java.lang.String> mods)

Method Summary

Modifier and Type	Method and Description
void	addAssignable(PositionedString ps)
void	addFreeInvariant(PositionedString ps)
void	addInfFlowSpecs(ImmutableList<PositionedString> l)
void	addInfFlowSpecs(PositionedString ps)
void	addInvariant(PositionedString ps)
boolean	equals(java.lang.Object o)
ImmutableList<PositionedString>	getAssignable()
ImmutableList<PositionedString>	getAssignable(java.lang.String hName)
java.util.Map<java.lang.String,ImmutableList<PositionedString>>	getAssignables()
java.util.Map<java.lang.String,ImmutableList<PositionedString>>	getFreeInvariants()
ImmutableList<PositionedString>	getInfFlowSpecs()
java.util.Map<java.lang.String,ImmutableList<PositionedString>>	getInvariants()
PositionedString	getVariant()
int	hashCode()
void	setVariant(PositionedString ps)
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct

addGeneric, getApproxPosition, getMods, getSourceFileName, isLoopContract, setLoopContract, setPosition

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

variant

private PositionedString variant

assignables

private java.util.Map<java.lang.String,ImmutableList<PositionedString>> assignables

infFlowSpecs

private ImmutableList<PositionedString> infFlowSpecs

invariants

private java.util.Map<java.lang.String,ImmutableList<PositionedString>> invariants

freeInvariants

private java.util.Map<java.lang.String,ImmutableList<PositionedString>> freeInvariants

Constructor Detail

TextualJMLLoopSpec

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

Method Detail

addInvariant

public void addInvariant(PositionedString ps)

addFreeInvariant

public void addFreeInvariant(PositionedString ps)

addAssignable

public void addAssignable(PositionedString ps)

addInfFlowSpecs

public void addInfFlowSpecs(PositionedString ps)

addInfFlowSpecs

public void addInfFlowSpecs(ImmutableList<PositionedString> l)

setVariant

public void setVariant(PositionedString ps)

getAssignable

public ImmutableList<PositionedString> getAssignable()

getAssignable

public ImmutableList<PositionedString> getAssignable(java.lang.String hName)

getAssignables

public java.util.Map<java.lang.String,ImmutableList<PositionedString>> getAssignables()

getInfFlowSpecs

public ImmutableList<PositionedString> getInfFlowSpecs()

getInvariants

public java.util.Map<java.lang.String,ImmutableList<PositionedString>> getInvariants()

getFreeInvariants

public java.util.Map<java.lang.String,ImmutableList<PositionedString>> getFreeInvariants()

getVariant

public PositionedString getVariant()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object