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-cases 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.