public final class TextualJMLLoopSpec extends TextualJMLConstruct
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 |
mods, name
Constructor and Description |
---|
TextualJMLLoopSpec(ImmutableList<java.lang.String> mods) |
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() |
addGeneric, getApproxPosition, getMods, getSourceFileName, isLoopContract, setLoopContract, setPosition
private PositionedString variant
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> assignables
private ImmutableList<PositionedString> infFlowSpecs
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> invariants
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> freeInvariants
public TextualJMLLoopSpec(ImmutableList<java.lang.String> mods)
public void addInvariant(PositionedString ps)
public void addFreeInvariant(PositionedString ps)
public void addAssignable(PositionedString ps)
public void addInfFlowSpecs(PositionedString ps)
public void addInfFlowSpecs(ImmutableList<PositionedString> l)
public void setVariant(PositionedString ps)
public ImmutableList<PositionedString> getAssignable()
public ImmutableList<PositionedString> getAssignable(java.lang.String hName)
public java.util.Map<java.lang.String,ImmutableList<PositionedString>> getAssignables()
public ImmutableList<PositionedString> getInfFlowSpecs()
public java.util.Map<java.lang.String,ImmutableList<PositionedString>> getInvariants()
public java.util.Map<java.lang.String,ImmutableList<PositionedString>> getFreeInvariants()
public PositionedString getVariant()
public java.lang.String toString()
toString
in class java.lang.Object
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object