The lcpp-primary pre
stands for the state just before
the invocation of the function being specified.
The lcpp-primary post
stands for the state just after that function's return.
The lcpp-primary any can be used when either of these will do,
and in invariants.
Each of these has the sort State,
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 State
that defines the sort State.
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.