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.