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.