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.