As in the refinement calculus
[Back88] [Back-vonWright89a] [Morgan94] [Morris87],
besides stating a specification using pre- and postconditions,
one can also state a specification as an abstract program.
The syntax for this in Larch/C++ is to use the keywords behavior program
followed by a compound statement.
Typically, such a compound statement would use specification-only variables
(see section 9.1 Ghost Variables) and specification statements,
so as to keep the specification as abstract as possible.
Specification statements are added to the usual C++ statements for this
purpose. They include assert statements and various clauses
from the grammar for fun-spec-body,
as well as a fun-spec-body itself
(see section 6 Function Specifications for the syntax of these).
specification-statement ::= fun-spec-body
| requires-clause
| accesses-clause
| modifies-clause
| trashes-clause
| calls-clause
| ensures-clause
| assert [ redundantly ] predicate ;
| assume-statement
| nondeterministic-choice
| nondeterministic-if
assume-statement ::= assume [ redundantly ] predicate ;
nondeterministic-choice ::= choose compound-statement [ or compound-statement ] ...
nondeterministic-if ::= if guarded-statement [ or guarded-statement ] ... [ else compound-statement ]
guarded-statement ::= { assume-statement [ statement-seq ] }
The meaning of a fun-spec-body as a statement is that, the code that replaces the fun-spec-body must satisfy the given specification. In terms of an execution, this means that if the precondition is true, the statement can, by making the changes allowed by the frame, achieve the given postcondition; thus, if the precondition is not true in the current state, then this statement can do anything at all. (For a fun-spec-body with several specification cases, the above applies to the desugared form.)
The meaning of an assert statement of the form
assert B;
is the same as
behavior {
requires B;
ensures true;
also
requires ~B;
ensures liberally false;
}
That is, if the given predicate is true in the given state,
this does nothing (skips), otherwise it aborts.
In the predicate of an assert statement,
the current state's value of a variable is referred to using the notation
for post-state values (').
(The pre-state's value is still referred to using the usual (^)
notation. See section 6.2.1 State Functions for more details.)
The meaning of
requires Pre;
is the same as
assert Pre;
The only difference between the assert statement
and a requires-clause used as a statement is that
in an requires-clause one can only refer to the pre-state
values of variables.
A requires-clause thus only is sensible as the first statement
in a function.
Similarly, the meaning of
ensures Post;
is the same as
assert Post;
That is, the meaning of an ensures-clause
is that the given postcondition must describe a true relationship
between the pre-state values of variables and
the current state's values (again written using the usual post-state
notation).
Typically you would only use an ensures-clause
at the end of a function, and use assert statements
for intermediate assertions.
The meaning of an assume-statement of the form
assume B;
is the same as
behavior { ensures B; }
Note that no objects may be trashed or modified,
because the default frame does not allow anything to be trashed
or modified.
That is, assume B; means that if the predicate B is true
in the current state, then the statement does nothing (skips),
otherwise it does not execute.
In either case, B is true after the statement executes,
since when B is not true, execution does not reach the
following statement (see p. 17 of [Hesselink92]).
An assume-statement is often used as a guard. The meaning of
assume B; S
is that if B is true in the current state,
then the statement S is executed, otherwise no execution takes place
[Nelson89] [Hesselink92].
We say a guard is enabled if B holds in the current state.
Larch/C++ has a special syntactic form of guarded statements that are used in nondeterministic-if statements. The meaning of a nondeterministic-if statement of the form
if { assume B1; SS1 } or ... or { assume Bn; SSn }
is that if none of the guards are enabled,
then the statement aborts;
otherwise, from among the enabled guards,
one is chosen, say Bi,
and the corresponding statement sequence, SSi, is executed.
If the optional else clause is present
then a nondeterministic-if statement will not abort
due to lack of enabled guards;
this is because
if { assume B1; SS1 } or ... or { assume Bn; SSn } else Se
is equivalent to
if { assume B1; SS1 } or ... or { assume Bn; SSn } or { assume true; Se }
The meaning of a nondeterministic-choice statement is that one of the compound-statements are nondeterministically chosen to execute. It follows that a nondeterministic-choice statement of the form:
choose { SS1 } or ... or { SSn }
is the same as
if { assume true; SS1 } or ... or { assume true; SSn }
The meaning of the accesses-clause, modifies-clause, trashes-clause, calls-clause is that the given constraint must be satisfied in the current state (with respect to the pre-state). For example, a modifies-clause says that since the beginning of the function's execution, only the given objects have been modified. Note that omitting one of these clauses in a behavior program is akin to not having any restriction at all; this is different than the usual notion of omitting a modifies-clause or trashes-clause.
As a very simple example of a behavior program,
consider the specification of inc4 below.
This specification says that a correct implementation of inc4
must behave as a refinement of the abstract program that is given.
Specifically, it may assume that the reference parameter i is assigned
in the pre-state, and then it can increment the value of i by 4,
provided that this will not cause an overflow, otherwise it must throw
Overflow.
// @(#)$Id: inc4.lh,v 1.4 1999/03/04 23:15:33 leavens Exp $
#include "Overflow.lh"
extern void inc4(int& i) throw(Overflow*);
//@ behavior program {
//@ requires assigned(i, pre);
//@ if (i + 4 <= INT_MAX) {
//@ i += 4;
//@ } else {
//@ assert i^ + 4 > INT_MAX;
//@ throw new Overflow();
//@ }
//@ }
The reader may wish to compare the above specification of inc4
with that of inc2 above
(see section 6.11 Exceptions).
One good use for a behavior program is to specify higher-order functions.
For example, consider the ArrayMap example above
(see section 6.13 Specifying Higher-Order Functions).
One may specify this using a behavior program, yielding a specification
that is significantly shorter than that given using a higher-order comparison.
// @(#)$Id: ArrayMap2.lh,v 1.1 1999/03/04 04:21:06 leavens Exp $
typedef int (*int_fun)(int) throw();
extern void ArrayMap(int a[], int len, int_fun fun) throw();
//@ behavior program {
//@ for (int i = 0; i < len; i++) {
//@ a[i] = (*fun)(a[i]);
//@ }
//@ }
The possible disadvantages of using a behavior program include that it may be more difficult to reason about, and a potential for implementation bias [Jones86b].
Go to the first, previous, next, last section, table of contents.