Sometimes functions are best specified in several different cases.
To allow this, a spec-case-seq in a function specification
may have multiple spec-cases separated by the keyword also.
Recall that there are two forms of a spec-case (see section 6 Function Specifications). The simplest has the following syntax, and contains all the elements discussed so far in this chapter.
[ let-clause ] req-frame-ens [ example-seq ]
There is also a form of a spec-case that allows for internal nesting of a spec-case-seq. The syntax is as follows.
[ let-clause ] [ requires-clause-seq ]{spec-case-seq}[ ensures-clause-seq ] [ example-seq ]
This second form is useful if a let-clause, requires-clause, ensures-clause or example-seq should be applied to several spec-cases.
The meaning of a function specification with more than one spec-case
in its spec-case-seq
is that the function has to satisfy each spec-case in the list.
The same idea gives the meaning of a nested spec-case-seq.
Both kinds of specification can be regarded as syntactic sugar
for a specification with only one spec-case,
as will be described below.
As an example of the use of multiple cases, and then of the translation into a specification without multiple cases, consider the following.
// @(#)$Id: widen1.lh,v 1.10 1997/06/03 20:30:26 leavens Exp $
extern void widen(int i) throw();
//@ behavior {
//@ extern int low_bound, high_bound;
//@ // "normal" case
//@ requires assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@ /\ INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i;
//@ modifies low_bound, high_bound;
//@ ensures (high_bound' - low_bound') = (high_bound^ - low_bound^) + i
//@ /\ low_bound' <= low_bound^ /\ high_bound^ <= high_bound';
//@ also // other cases
//@ requires assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@ /\ INT_MIN + i >= low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i;
//@ modifies high_bound;
//@ ensures high_bound' = high_bound^ + i;
//@ also
//@ requires assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@ /\ INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ >= INT_MAX - i;
//@ modifies low_bound;
//@ ensures low_bound' = low_bound^ - i;
//@ }
In the "normal" case the function widen
is expected to make the difference
between low_bound and high_bound
greater by the value of the formal parameter i.
It can do this by either changing low_bound
or high_bound or both.
The other cases say that when low_bound is two small, high_bound
must be increased, and vice versa.
An equivalent desugared version of the above specification is the following. This specification shows the general way to translate a spec-case-seq into a single spec-case. The general idea is to: form the single precondition by disjoining the preconditions of the cases, list in the single modifies-clause everything listed in each of the modifies-clauses of the cases, and form the single postcondition from the conjunction of implications, with each implication being of one case's precondition implying the postcondition of that case conjoined with an assertion saying that everything is unchanged which is not listed in the modifies-clause for that case.
// @(#)$Id: widen2.lh,v 1.13 1997/06/03 20:30:27 leavens Exp $
extern void widen(int i) throw();
//@ behavior { // a desugared version of widen1
//@ extern int low_bound, high_bound;
//@ requires (assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@ /\ INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i)
//@ \/ (assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@ /\ INT_MIN + i >= low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i)
//@ \/ (assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@ /\ INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ >= INT_MAX - i);
//@ modifies low_bound, high_bound;
//@ ensures ((assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@ /\ INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i)
//@ => ((high_bound' - low_bound')
//@ = (high_bound^ - low_bound^) + i
//@ /\ low_bound' <= low_bound^
//@ /\ high_bound^ <= high_bound'))
//@ /\ ((assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@ /\ INT_MIN + i >= low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i)
//@ => (high_bound' = high_bound^ + i /\ unchanged(low_bound)))
//@ /\ ((assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@ /\ INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ >= INT_MAX - i)
//@ => (low_bound' = low_bound^ - i /\ unchanged(high_bound)));
//@ }
If the spec-cases of a spec-case-seq have let-clauses, then these are first desugared before the above translation is applied.
The first specification of widen given above is less compact than
it could be, because the first two conjuncts of each spec-case's
requires-clause are the same.
Also, since the variables low_bound and high_bound occur
so frequently in the specification, it is convenient to abbreviate them
using a let-clause.
The following specification of widen
uses these ideas to give a more compact specification
of widen.
// @(#)$Id: widen3.lh,v 1.6 1998/08/27 22:56:52 leavens Exp $
extern void widen(int i) throw();
//@ behavior {
//@ extern int low_bound, high_bound;
//@
//@ let lb: Obj[int] be low_bound, hb: Obj[int] be high_bound;
//@ requires assigned(lb, pre) /\ assigned(hb, pre);
//@ {
//@ requires INT_MIN + i < lb^ /\ lb^ < hb^ /\ hb^ < INT_MAX - i;
//@ modifies lb, hb;
//@ ensures (hb' - lb') = (hb^ - lb^) + i /\ lb' <= lb^ /\ hb^ <= hb';
//@
//@ also // other cases
//@
//@ requires INT_MIN + i >= lb^ /\ lb^ < hb^ /\ hb^ < INT_MAX - i;
//@ modifies hb;
//@ ensures hb' = hb^ + i;
//@
//@ also
//@
//@ requires INT_MIN + i < lb^ /\ lb^ < hb^ /\ hb^ >= INT_MAX - i;
//@ modifies lb;
//@ ensures lb' = lb^ - i;
//@ }
//@ ensures redundantly inRange(lb') /\ inRange(hb');
//@ example 8 < INT_MAX /\ i = 2 /\ lb^ = 3 /\ hb^ = 6
//@ /\ lb' = 1 /\ hb' = 6;
//@ example 8 < INT_MAX /\ i = 2 /\ lb^ = 3 /\ hb^ = 6
//@ /\ lb' = 3 /\ hb' = 8;
//@ example 8 < INT_MAX /\ i = 2 /\ lb^ = 3 /\ hb^ = 6
//@ /\ lb' = 2 /\ hb' = 7;
//@ }
As illustrated in the above example, the potential scope of a definition made in a let-clause is its entire spec-case, this includes nested spec-cases.
Also illustrated by the above example is that a requires-clause applies to nested spec-cases by conjunction; that is, such a requires-clause is conjoined to the requires-clause of each nested spec-case.
If there are multiple, non-redundant requires-clauses or ensures-clauses in a requires-clause-seq, or ensures-clause-seq in a spec-case, these are first conjoined to make each spec-case have a single non-redundant such clause.
The redundant ensures clause and the examples
given in the last specification of widen above apply
to the entire specification case.
That is, they apply to the meaning of a spec-case with a nested
spec-case-seq.
Such a specification can be translated into a specification with just one spec-case by first desugaring the nested spec-case-seq, then conjoining the requires-clause to the desugared requires-clause. If desired, one could also then desugar the let-clause.
For example, the last specification of widen above
is equivalent to the following.
// @(#)$Id: widen4.lh,v 1.8 1998/08/27 22:56:53 leavens Exp $
extern void widen(int i) throw();
//@ behavior {
//@ extern int low_bound, high_bound;
//@ requires (assigned(low_bound, pre) /\ assigned(high_bound, pre))
//@ /\ ( (INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i)
//@ \/ (INT_MIN + i >= low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i)
//@ \/ (INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ >= INT_MAX - i) );
//@ modifies low_bound, high_bound;
//@ ensures ((INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i)
//@ => ((high_bound' - low_bound')
//@ = (high_bound^ - low_bound^) + i
//@ /\ low_bound' <= low_bound^ /\ high_bound^ <= high_bound'))
//@ /\ ((INT_MIN + i >= low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ < INT_MAX - i)
//@ => (high_bound' = high_bound^ + i /\ unchanged(low_bound)))
//@ /\ ((INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@ /\ high_bound^ >= INT_MAX - i)
//@ => (low_bound' = low_bound^ - i /\ unchanged(high_bound)));
//@ ensures redundantly inRange(low_bound') /\ inRange(high_bound');
//@ example 8 < INT_MAX /\ i = 2 /\ low_bound^ = 3 /\ high_bound^ = 6
//@ /\ low_bound' = 1 /\ high_bound' = 6;
//@ example 8 < INT_MAX /\ i = 2 /\ low_bound^ = 3 /\ high_bound^ = 6
//@ /\ low_bound' = 3 /\ high_bound' = 8;
//@ example 8 < INT_MAX /\ i = 2 /\ low_bound^ = 3 /\ high_bound^ = 6
//@ /\ low_bound' = 2 /\ high_bound' = 7;
//@ }
Redundant clauses need not appear in the translation of a case analysis, as they are not needed to give meaning to the specification. Still, it may be informative (or fun) to include them. Examples are easily taken care of by combining all the examples into one large example-seq in the translation. Redundant ensures-clauses are all listed after the non-redundant ensures-clause, but with their post-conds changed into implications. The hypothesis of such an implication is the precondition of its original spec-case, and the antecedent is the original predicate of the claims-clause.
Redundant requires-clauses are more tricky. They can be translated by conjoining all the pre-conds for each spec-case together, and then disjoining the resulting conjunctions to form a single pre-cond for a single redundant requires-clause.
See section 6.11 Exceptions for more examples of case analysis.
This feature of Larch/C++ is inspired by various versions of refinement for function specifications. The simple case of a spec-case-seq without nesting is nearly identical to the mechanism found in Section 4.1.4 of [Wing83], and is similar to the capsule mechanism of [Wills92b].
Go to the first, previous, next, last section, table of contents.