de.uka.ilkd.key.speclang

Class WellDefinednessCheck.POTerms

java.lang.Object

de.uka.ilkd.key.speclang.WellDefinednessCheck.POTerms

Enclosing class:

WellDefinednessCheck

public static final class WellDefinednessCheck.POTerms
extends java.lang.Object

A data structure for storing and passing all specifications of a specification element includinf pre- and post-condition, an assignable-clause and a list of all other clauses specified.

Author:

Michael Kirsten

Field Summary

Fields

Modifier and Type	Field and Description
Term	mod
WellDefinednessCheck.Condition	post
WellDefinednessCheck.Condition	pre
ImmutableList<Term>	rest

Constructor Summary

Constructors

Constructor and Description
POTerms(WellDefinednessCheck.Condition pre, Term mod, ImmutableList<Term> rest, WellDefinednessCheck.Condition post)

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

pre

public final WellDefinednessCheck.Condition pre

mod

public final Term mod

rest

public final ImmutableList<Term> rest

post

public final WellDefinednessCheck.Condition post

Constructor Detail

POTerms

POTerms(WellDefinednessCheck.Condition pre,
        Term mod,
        ImmutableList<Term> rest,
        WellDefinednessCheck.Condition post)