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

6.14 Behavior Programs

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;
       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.