An `example-seq` can be used to give the reader a concrete example
of the behavior of a function.
Such examples do not change the meaning of a specification,
and could, of course, be written as comments in a specification.
However, by making examples part of a Larch/C++ specification,
one introduces checkable redundancy.
That is, it one can check that the
relationship between the pre- and post-states described in the example
satisfies the specification.

The syntax is as follows.

example-seq::=example[example] ...example::=`example`

[`liberally`

]predicate`;`

For example, in the following, the example listed shows the effect of transferring 100 dollars from the source account to the sink account.

// @(#)$Id: transfer3.lh,v 1.10 1997/07/24 21:14:07 leavens Exp $ #include "BankAccount.lh" extern void transfer(BankAccount& source, BankAccount& sink, Money amt) throw(); //@ behavior { //@ requires source ~= sink /\ assigned(sink, pre) /\ assigned(source, pre) //@ /\ source^.credit^ >= amt /\ amt >= 0; //@ modifies source^.credit, sink^.credit; //@ ensures sink'.credit' = sink^.credit^ + amt //@ /\ source'.credit' = souce^.credit^ - amt; //@ example amt = money(100/1) //@ /\ source^.credit^ = money(500/1) /\ sink^.credit^ = money(200/1) //@ /\ source'.credit' = money(400/1) /\ sink'.credit' = money(300/1); //@ }

A pair of example states would satisfy a specification when the pre-state violates the precondition; and in such an example, the poststate need not satisfy the postcondition. However, psychologically, such an example would be confusing, and so such examples are to be avoided. An example could also be confusing by violating the specified frame; and so that should be avoided as well.

You can check that an example does not violate the precondition
and frame of the example.
by checking the consistency of the following formula.
That is, what should be checked to validate the consistency of an
example with respect to the `spec-case`
is the following,
where `PreCondition`

is the `spec-case`'s (desugared) precondition,
`MP`

is the predicate that codes its `modifies-clause`
(see section 6.2.3 The Modifies Clause),
`TP`

is the predicate that codes its `trashes-clause`
(see section 6.3.2 The Trashes Clause),
and `Example`

is the predicate from the `example`.

Example /\ PreCondition /\ MP /\ TP

One way to prove the consistency of such a formula is to prove
that this formula does not imply `false`

.
One can also construct a pair of states that satisfies it.

When a specification does not completely determine the result of a function
(i.e., when it is **incomplete**),
one should give several examples.
Otherwise readers who are not careful
may assume that the single example given illustrates all the possibilities.
For example, the following gives two examples for the integer square root
specification.

// @(#)$Id: isqrt2.lh,v 1.6 1997/09/16 03:03:30 leavens Exp $ extern int isqrt(int x) throw(); //@ behavior { //@ requires x >= 0; //@ ensures (result-1)*(result-1) < x //@ /\ x < (result+1)*(result+1); //@ example x = 28 /\ result = 5; //@ example x = 28 /\ result = 6; //@ }

The semantics of an `example` that does not use `liberally`

is that,
for all pairs of pre and post states,
if the pair of states satisfies the
conjunction of the predicate in the example,
the precondition for the `spec-case` to which the example is
attached,
and its `frame`,
then the pair should also satisfy the postcondition of that `spec-case`.
That is, what should be checked to debug an example
is the following,
where `Example`

, `PreCondition`

, `MP`

and `TP`

are as above,
and `PostCondition`

is the postcondition of the `spec-case`.

(Example /\ PreCondition /\ MP /\ TP) => PostCondition

In cases where there are applicable invariants (see section 7.3 Class Invariants)
or history constraints (see section 7.4 History Constraints)
these may be instantiated for whatever objects are assigned
in the pre-state and conjoined to the hypothesis of the above formula.
Thus, for example, in a class specification,
one might prove the following,
where
`Invariant(pre)`

is the invariant
with the to the pre-state (`pre`

) substituted for
the state `any`

used to express the invariant.

(Example /\ PreCondition /\ Invariant(pre) /\ MP /\ TP) => PostCondition

The meaning for an `example` that uses `liberally`

is the same, except that termination is not implied.
(See section 6.12 Liberal Specifications for more on this topic and an example.)

Such a proof should be carried out for each `example`
in the `example-seq`.

The reason for including the predicates describing the `frame`
in the hypothesis, is to allow more succinct and less error-prone
examples. (Without the frame axioms, most examples would have
to state that each object was assigned in the post-state.)

Go to the first, previous, next, last section, table of contents.