Until this point, we have ignored the possibility of one writing an
`ensures-clause` (see section 6 Function Specifications) of the following form.

`ensures`

`liberally`

post-cond`;`

Such an `ensures-clause` gives
a partial-correctness specification, as opposed to the usual
total-correctness specification [Dijkstra76].
In a **partial-correctness specification**,
if the precondition holds and if the function terminates
(see section 6.12.1 Terminates),
then the `post-cond` must hold;
however, normal termination is not guaranteed,
even when the precondition holds.

In Larch/C++, a `spec-case` that uses the keyword
`liberally`

will be called a **partial-correctness** `spec-case`.
A **total-correctness** `spec-case` is one that does not use
the keyword `liberally`

.
It guarantees normal termination for all pre-states for which
its precondition holds.

As an example of a liberal or partial-correctness specification, consider the following specification of a factorial function. The function specified need not terminate normally when called with any arguments (as noted in the third example), but if it does terminate, then the result must be the factorial of the argument.

// @(#)$Id: fact_liberal.lh,v 1.6 1997/06/03 20:30:03 leavens Exp $ extern int fact_liberal(int n) throw(); //@ behavior { //@ uses FactorialTrait; //@ ensures liberally result = factorial(n); //@ example liberally n = 3 /\ result = 6; //@ example liberally n = -2 /\ result = 1; //@ example liberally false; //@ }

The `predicate` `false`

can be used in a liberal example
to say that no post-state exists.
This is used in the third example of the `fact_liberal`

function specified above.

A valid implementation of the specification of `fact_liberal`

would be an infinite loop;
another implementation would loop only on negative arguments.
An implementation that halts the program (on some arguments) would also
be acceptable.

The above specification uses the trait `FactorialTrait`

,
which itself uses the trait `int`

(see section 11.1.5 int Trait).
Note that factorials of negative numbers are defined to be 1.

% @(#)$Id: FactorialTrait.lsl,v 1.1 1995/06/12 20:39:34 leavens Exp $ FactorialTrait: trait includes int introduces factorial: int -> int asserts \forall n: int factorial(n) == if n <= 0 then 1 else n * factorial(n-1)

- Terminates
- Liberal Specification and Case Analysis
- Examples of Liberal Specification
- Meaning of Function Specifications

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