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