- 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