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


6.12.2 Liberal Specification and Case Analysis

Liberal specification can be combined with case analysis. For example, suppose one wanted to specify that fact_liberal2 must terminate normally when its argument is sensible. This could be specified as follows.

// @(#)$Id: fact_liberal2.lh,v 1.6 1997/06/03 20:30:04 leavens Exp $

extern int fact_liberal2(int n) throw();
//@ behavior {
//@   uses FactorialTrait;
//@
//@   requires 0 <= n /\ factorial(n) <= INT_MAX;
//@   ensures result = factorial(n);
//@ also
//@   requires ~(0 <= n /\ factorial(n) <= INT_MAX);
//@   ensures liberally result = factorial(n);
//@ }

When discussing case analysis above, we presented a way to think of case analysis as syntactic sugar for a specification with a single spec-case (see section 6.10 Case Analysis). However, because partial-correctness and total-correctness specifications have different meanings, one cannot desugar a spec-case-seq with a mix of such spec-cases into a single spec-case. One can only desugar the specification into a spec-case-seq with two spec-cases: one for the total-correctness specification, and one for the partial-correctness specification. This is done by applying the syntactic sugaring given above for combining spec-cases separately to each kind of spec-case: total and partial. Hence, the above specification cannot be further desugared.

As an aside, by using standard techniques [Dijkstra76] [Nelson89] [Hesselink92], one can always rewrite such a specification so that it has one spec-case with an ensures-clause of the form ensures true and a second spec-case with an ensures-clause of the form ensures liberally P, for some post-cond P. For example, the following is equivalent to the above specification of fact_liberal2.

// @(#)$Id: fact_liberal3.lh,v 1.5 1997/06/03 20:30:05 leavens Exp $

extern int fact_liberal2(int n) throw();
//@ behavior {
//@   uses FactorialTrait;
//@
//@   requires 0 <= n /\ factorial(n) < INT_MAX;
//@   ensures true;
//@ also
//@   requires true;
//@   ensures liberally result = factorial(n);
//@ }

The meaning of a specification with multiple spec-cases is as always -- the function must satisfy all of them. In the above specification, this means that the function must terminate normally when the argument satisfies the requires-clause of the first spec-case, and that when it terminates, it must satisfy the ensures-clause of the second spec-case.


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