By using both total and partial-correctness spec-cases, one can specify interesting behaviors that would not be possible with just total-correctness specification. This can be done because one can precisely specify both when the function terminates and what must be true of the states in which it is allowed to terminate.
As an example of how to specify a function that
does not return to its caller,
consider the following specification
of the C++ library function abort
(see Section 3.4 of [Ellis-Stroustrup90]).
// @(#)$Id: abort.lh,v 1.6 1997/06/03 20:29:55 leavens Exp $
extern void abort() throw();
//@ behavior {
//@ requires false;
//@ ensures true;
//@ also
//@ requires true;
//@ ensures liberally false;
//@ }
The first spec-case in the above specification says:
there is no way to call abort so that it is guaranteed
to terminate normally.
The second spec-case says that furthermore:
every execution of abort either fails to terminate normally
or it terminates in a state in which false holds;
that means, of course, that it can never terminate normally,
because there is no state in which false holds.
However there is a potential execution, because the state
bottom does not represent normal termination.
Hence, as a relation, abort relates all states to bottom.
One can also specify functions that could not possibly be implemented,
but which may be useful in program refinement.
For example, the following is the specification of
the function miracle (see [Nelson89] and Section 1.3 of [Hesselink92]).
// @(#)$Id: miracle.lh,v 1.9 1997/01/04 16:58:57 leavens Exp $
extern void miracle();
//@ behavior {
//@ extern everything;
//@
//@ requires true;
//@ modifies everything;
//@ trashes everything;
//@ ensures true;
//@ also
//@ requires true;
//@ modifies everything;
//@ trashes everything;
//@ ensures liberally false;
//@ }
According to the total-correctness case of this specification,
every execution of a call to miracle
would have to terminate normally.
According to the partial-correctness case,
every such execution would have to terminate in a state in which false holds.
Since there are no such executions, such a function
would have to refuse to execute,
and thus could not be implemented in C++.
Go to the first, previous, next, last section, table of contents.