stands for the state just before
the invocation of the function being specified.
stands for the state just after that function's return.
any can be used when either of these will do,
and in invariants.
Each of these has the sort
which is the sort of the formal model of states in Larch/C++.
See section 2.8.2 Formal Model of States for details on the trait
that defines the sort
This feature of Larch/C++ was used in the specification language LM3 (Chapter 6 of [Guttag-Horning93], see Section 2.3.2 of [Jones91]). In LM3 [Jones91], Jones emphasizes the use of explicit states for specifying higher-order procedures.
Go to the first, previous, next, last section, table of contents.