Sometimes functions are best specified in several different cases.
To allow this, a `spec-case-seq` in a function specification
may have multiple `spec-case`s 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-case`s.

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-clause`s 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-case`s of a `spec-case-seq` have `let-clause`s,
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-case`s.

Also illustrated by the above example is that
a `requires-clause` applies to nested `spec-case`s 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-clause`s
or `ensures-clause`s 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-clause`s are all listed after the
non-redundant `ensures-clause`, but with
their `post-cond`s 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-clause`s are more tricky.
They can be translated by conjoining all the `pre-cond`s
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.