de.uka.ilkd.key.speclang.jml.translation

Class JMLSpecFactory.ContractClauses

java.lang.Object

de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.ContractClauses

Enclosing class:

JMLSpecFactory

private static class JMLSpecFactory.ContractClauses
extends java.lang.Object

Field Summary

Fields

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 Summary

Constructors

Modifier	Constructor and Description
private	ContractClauses()

Method Summary

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

abbreviations

public ImmutableList<Term> abbreviations

requires

public java.util.Map<LocationVariable,Term> requires

requiresFree

public java.util.Map<LocationVariable,Term> requiresFree

measuredBy

public Term measuredBy

decreases

public Term decreases

assignables

public java.util.Map<LocationVariable,Term> assignables

accessibles

public java.util.Map<ProgramVariable,Term> accessibles

ensures

public java.util.Map<LocationVariable,Term> ensures

ensuresFree

public java.util.Map<LocationVariable,Term> ensuresFree

axioms

public java.util.Map<LocationVariable,Term> axioms

signals

public Term signals

signalsOnly

public Term signalsOnly

diverges

public Term diverges

breaks

public java.util.Map<Label,Term> breaks

continues

public java.util.Map<Label,Term> continues

returns

public Term returns

hasMod

public java.util.Map<LocationVariable,java.lang.Boolean> hasMod

infFlowSpecs

public ImmutableList<InfFlowSpec> infFlowSpecs

Constructor Detail

ContractClauses

private ContractClauses()