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

6.12 Liberal Specifications

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)

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