Every function specification can be desugared into one with
only one total-correctness `spec-case`
and one partial-correctness `spec-case`.
A function with only one total correctness `spec-case`
can be rewritten into this form in the standard way
[Dijkstra76] [Nelson89] [Hesselink92]
(see section 6.12.2 Liberal Specification and Case Analysis for an example).
A specification with one or more partial correctness `spec-case`s can
be rewritten into one with a single partial correctness `spec-case`
by using the desugaring for case analysis (see section 6.10 Case Analysis);
then a total correctness `spec-case` of the following form
can be added, since this adds no information to the specification.

requires false; modifies everything; trashes everything; ensures true;

(The `frame` allows everything to be modified or trashed,
but that would ordinarily be restricted by the other `spec-case`.)

So to give the meaning of a function specification,
it suffices to consider a function specification
with one total-correctness `spec-case`
and one partial-correctness `spec-case` (one that uses `liberally`

).
A C++ function **satisfies its specification**
if and only if for each type-correct function call:
(i) if the precondition of the total-correctness case
is satisfied in the pre-state,
then the function call terminates,
the function mutates at most the set of objects
described in the total-correctness `modifies-clause`,
trashes at most the set of objects described in the
total-correctness `trashes-clause`,
and the total-correctness
postcondition is satisfied by the pre-state and the post-state,
and furthermore
(ii) if the precondition of the partial-correctness case
is satisfied in the pre-state,
and if the function call terminates,
then function mutates at most the set of objects
described in the partial-correctness `modifies-clause`,
trashes at most the set of objects described in the
partial-correctness `trashes-clause`,
and the partial-correctness
postcondition is satisfied by the pre-state and the post-state.

For specifications that do not use `liberally`

,
the above definition of satisfaction is the same as that as described previously
(see section 6.2.3 The Modifies Clause).

Go to the first, previous, next, last section, table of contents.