public final class TextualJMLSpecCase extends TextualJMLConstruct
Modifier and Type | Class and Description |
---|---|
static class |
TextualJMLSpecCase.Clause
Heap-independent clauses
|
static class |
TextualJMLSpecCase.ClauseHd
Heap-dependent clauses
|
mods, name
Constructor and Description |
---|
TextualJMLSpecCase(ImmutableList<java.lang.String> mods,
Behavior behavior) |
addGeneric, getApproxPosition, getMods, getSourceFileName, isLoopContract, setLoopContract, setPosition, setPosition, setPosition
public TextualJMLSpecCase(ImmutableList<java.lang.String> mods, @Nonnull Behavior behavior)
public ImmutableList<LabeledParserRuleContext> getRequiresFree(Name toString)
public ImmutableList<LabeledParserRuleContext> getEnsuresFree(Name toString)
public ImmutableList<LabeledParserRuleContext> getAccessible(Name heap)
public ImmutableList<LabeledParserRuleContext> getAxioms(Name heap)
public ImmutableList<LabeledParserRuleContext> getEnsures(Name heap)
public ImmutableList<LabeledParserRuleContext> getRequires(Name heap)
public ImmutableList<LabeledParserRuleContext> getAssignable(Name heap)
public ImmutableList<LabeledParserRuleContext> getDecreases()
public TextualJMLSpecCase addClause(TextualJMLSpecCase.Clause clause, LabeledParserRuleContext ctx)
public TextualJMLSpecCase addClause(TextualJMLSpecCase.ClauseHd clause, LabeledParserRuleContext ctx)
public TextualJMLSpecCase addClause(TextualJMLSpecCase.ClauseHd clause, @Nullable Name heapName, LabeledParserRuleContext ctx)
public TextualJMLSpecCase addClause(TextualJMLSpecCase.Clause clause, org.antlr.v4.runtime.ParserRuleContext ctx)
public TextualJMLSpecCase addClause(TextualJMLSpecCase.ClauseHd clause, org.antlr.v4.runtime.ParserRuleContext ctx)
public TextualJMLSpecCase addClause(TextualJMLSpecCase.ClauseHd clause, @Nullable Name heapName, org.antlr.v4.runtime.ParserRuleContext ctx)
@Nonnull public TextualJMLSpecCase merge(@Nonnull TextualJMLSpecCase other)
other
- @Nonnull public TextualJMLSpecCase clone()
clone
in class java.lang.Object
public void addName(java.lang.String n)
public Behavior getBehavior()
public java.lang.String getName()
public java.lang.String toString()
toString
in class java.lang.Object
public void addRequires(LabeledParserRuleContext label)
public Triple<LabeledParserRuleContext,LabeledParserRuleContext,LabeledParserRuleContext>[] getAbbreviations()
public ImmutableList<LabeledParserRuleContext> getInfFlowSpecs()
public ImmutableList<LabeledParserRuleContext> getReturns()
public ImmutableList<LabeledParserRuleContext> getContinues()
public ImmutableList<LabeledParserRuleContext> getBreaks()
public ImmutableList<LabeledParserRuleContext> getDiverges()
public ImmutableList<LabeledParserRuleContext> getMeasuredBy()
public ImmutableList<LabeledParserRuleContext> getSignalsOnly()
public ImmutableList<LabeledParserRuleContext> getRequires()
public ImmutableList<LabeledParserRuleContext> getAssignable()
public ImmutableList<LabeledParserRuleContext> getEnsures()
public ImmutableList<LabeledParserRuleContext> getSignals()
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.