public final class TextualJMLSpecCase extends TextualJMLConstruct
mods, name
Constructor and Description |
---|
TextualJMLSpecCase(ImmutableList<java.lang.String> mods,
Behavior behavior) |
addGeneric, getApproxPosition, getMods, getSourceFileName, isLoopContract, setLoopContract, setPosition
private final Behavior behavior
private PositionedString workingSpace
private ImmutableList<PositionedString> measuredBy
private ImmutableList<PositionedString> signals
private ImmutableList<PositionedString> signalsOnly
private ImmutableList<PositionedString> diverges
private ImmutableList<PositionedString> depends
private ImmutableList<PositionedString> breaks
private ImmutableList<PositionedString> continues
private ImmutableList<PositionedString> returns
private ImmutableList<PositionedString> decreases
private ImmutableList<Triple<PositionedString,PositionedString,PositionedString>> abbreviations
private ImmutableList<PositionedString> infFlowSpecs
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> accessibles
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> assignables
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> requires
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> requiresFree
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> ensures
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> ensuresFree
private java.util.Map<java.lang.String,ImmutableList<PositionedString>> axioms
public TextualJMLSpecCase(ImmutableList<java.lang.String> mods, Behavior behavior)
public static TextualJMLSpecCase assert2blockContract(ImmutableList<java.lang.String> mods, PositionedString assertStm)
public TextualJMLSpecCase merge(TextualJMLSpecCase tsc)
tsc
- public TextualJMLSpecCase clone()
clone
in class java.lang.Object
public void addName(PositionedString n)
public void addRequires(PositionedString ps)
public void addRequires(ImmutableList<PositionedString> l)
public void addRequiresFree(PositionedString ps)
public void addRequiresFree(ImmutableList<PositionedString> l)
public void addMeasuredBy(PositionedString ps)
public void addMeasuredBy(ImmutableList<PositionedString> l)
public void addDecreases(PositionedString ps)
public void addDecreases(ImmutableList<PositionedString> l)
public void addAssignable(PositionedString ps)
public void addAssignable(ImmutableList<PositionedString> l)
public void addAccessible(PositionedString ps)
public void addAccessible(ImmutableList<PositionedString> l)
public void addEnsures(PositionedString ps)
public void addEnsures(ImmutableList<PositionedString> l)
public void addEnsuresFree(PositionedString ps)
public void addEnsuresFree(ImmutableList<PositionedString> l)
public void addSignals(PositionedString ps)
public void addSignals(ImmutableList<PositionedString> l)
public void addSignalsOnly(PositionedString ps)
public void addSignalsOnly(ImmutableList<PositionedString> l)
public void setWorkingSpace(PositionedString ps)
public void addDiverges(PositionedString ps)
public void addDiverges(ImmutableList<PositionedString> l)
public void addDepends(PositionedString ps)
public void addBreaks(PositionedString ps)
public void addBreaks(ImmutableList<PositionedString> l)
public void addContinues(PositionedString ps)
public void addContinues(ImmutableList<PositionedString> l)
public void addReturns(PositionedString ps)
public void addReturns(ImmutableList<PositionedString> l)
public void addAbbreviation(PositionedString[] pss)
public void addAxioms(PositionedString ps)
public void addAxioms(ImmutableList<PositionedString> l)
public void addInfFlowSpecs(PositionedString ps)
public void addInfFlowSpecs(ImmutableList<PositionedString> l)
public Behavior getBehavior()
public ImmutableList<PositionedString> getRequires()
public ImmutableList<PositionedString> getRequires(java.lang.String hName)
public ImmutableList<PositionedString> getRequiresFree()
public ImmutableList<PositionedString> getRequiresFree(java.lang.String hName)
public ImmutableList<PositionedString> getMeasuredBy()
public ImmutableList<PositionedString> getDecreases()
public ImmutableList<PositionedString> getAssignable()
public ImmutableList<PositionedString> getAssignable(java.lang.String hName)
public ImmutableList<PositionedString> getAccessible()
public ImmutableList<PositionedString> getAccessible(java.lang.String hName)
public ImmutableList<PositionedString> getEnsures()
public ImmutableList<PositionedString> getEnsures(java.lang.String hName)
public ImmutableList<PositionedString> getEnsuresFree()
public ImmutableList<PositionedString> getEnsuresFree(java.lang.String hName)
public ImmutableList<PositionedString> getAxioms()
public ImmutableList<PositionedString> getAxioms(java.lang.String hName)
public java.lang.String getName()
public ImmutableList<PositionedString> getSignals()
public ImmutableList<PositionedString> getSignalsOnly()
public PositionedString getWorkingSpace()
public ImmutableList<PositionedString> getDiverges()
public ImmutableList<PositionedString> getDepends()
public ImmutableList<PositionedString> getBreaks()
public ImmutableList<PositionedString> getContinues()
public ImmutableList<PositionedString> getReturns()
public ImmutableList<Triple<PositionedString,PositionedString,PositionedString>> getAbbreviations()
public ImmutableList<PositionedString> getInfFlowSpecs()
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