private static class JMLSpecFactory.ContractClauses
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
ImmutableList<Term> |
abbreviations |
java.util.Map<ProgramVariable,Term> |
accessibles |
java.util.Map<LocationVariable,Term> |
assignables |
java.util.Map<LocationVariable,Term> |
axioms |
java.util.Map<Label,Term> |
breaks |
java.util.Map<Label,Term> |
continues |
Term |
decreases |
Term |
diverges |
java.util.Map<LocationVariable,Term> |
ensures |
java.util.Map<LocationVariable,Term> |
ensuresFree |
java.util.Map<LocationVariable,java.lang.Boolean> |
hasMod |
ImmutableList<InfFlowSpec> |
infFlowSpecs |
Term |
measuredBy |
java.util.Map<LocationVariable,Term> |
requires |
java.util.Map<LocationVariable,Term> |
requiresFree |
Term |
returns |
Term |
signals |
Term |
signalsOnly |
Modifier | Constructor and Description |
---|---|
private |
ContractClauses() |
public ImmutableList<Term> abbreviations
public java.util.Map<LocationVariable,Term> requires
public java.util.Map<LocationVariable,Term> requiresFree
public Term measuredBy
public Term decreases
public java.util.Map<LocationVariable,Term> assignables
public java.util.Map<ProgramVariable,Term> accessibles
public java.util.Map<LocationVariable,Term> ensures
public java.util.Map<LocationVariable,Term> ensuresFree
public java.util.Map<LocationVariable,Term> axioms
public Term signals
public Term signalsOnly
public Term diverges
public Term returns
public java.util.Map<LocationVariable,java.lang.Boolean> hasMod
public ImmutableList<InfFlowSpec> infFlowSpecs