de.uka.ilkd.key.speclang

Class StatementWellDefinedness.SequentTerms

java.lang.Object

de.uka.ilkd.key.speclang.StatementWellDefinedness.SequentTerms

Enclosing class:

StatementWellDefinedness

final class StatementWellDefinedness.SequentTerms
extends java.lang.Object

A data structure to pass the needed terms for the well-definedness sequent of a jml statement, including the context update, pre-condition for the statement, well-formedness condition for the anonymous heap, well-definedness term for the statement's assignable-clause, well-definedness term for other clauses in the statement and the well-definedness term for the statement's post-condition with the according updates (heap of pre-state becomes current heap and the current heap gets anonymised) applied to it.

Author:

Michael Kirsten

Field Summary

Fields

Modifier and Type	Field and Description
(package private) Term	anonWdPost
(package private) Term	context
(package private) Term	pre
(package private) Term	wdMod
(package private) Term	wdRest
(package private) Term	wfAnon

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SequentTerms(Term context, Term pre, Term anonHeap, Term mod, ImmutableList<Term> rest, Term anonWdPost, TermServices services)

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

context

final Term context

pre

final Term pre

wfAnon

final Term wfAnon

wdMod

final Term wdMod

wdRest

final Term wdRest

anonWdPost

final Term anonWdPost

Constructor Detail

SequentTerms

private SequentTerms(Term context,
                     Term pre,
                     Term anonHeap,
                     Term mod,
                     ImmutableList<Term> rest,
                     Term anonWdPost,
                     TermServices services)