public 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 |
Constructor and Description |
---|
ContractClauses() |
Modifier and Type | Method and Description |
---|---|
void |
clear() |
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
Copyright © 2003-2019 The KeY-Project.