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-case`s
into a single `spec-case`.
One can only desugar the specification into a `spec-case-seq` with two
`spec-case`s: 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-case`s
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.