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

6 Function Specifications

A Larch/C++ function specification has two parts: an interface specification, and a behavioral specification. The interface is specified by a C++ declaration, and the behavioral specification is attached to it, following the keywords behavior or behavior program. Technically, a fun-spec-body may be written in the places noted in the syntax for declaration above. (See section 5 Declarations for the syntax.) Many examples are given in this chapter.

fun-spec-body ::= behavior { [ uses-seq ] [ declaration-seq ] spec-case-seq }
        | behavior program compound-statement
uses-seq ::= uses-clause [ uses-clause ] ...
spec-case-seq ::= spec-case [ also spec-case ] ...
spec-case ::= [ let-clause ] req-frame-ens [ example-seq ]
        | [ let-clause ] [ requires-clause-seq ] { spec-case-seq }  [ ensures-clause-seq ] [ example-seq ]
req-frame-ens ::= [ requires-clause-seq ] ensures-clause-seq
      | [ requires-clause-seq ] frame [ ensures-clause-seq ]
requires-clause-seq ::= requires-clause [ requires-clause ] ...
requires-clause ::= requires [ redundantly ] pre-cond ;
pre-cond ::= predicate
frame ::= accesses-clause-seq [ modifies-clause-seq ] [ trashes-clause-seq ] [ calls-clause-seq ]
        | modifies-clause-seq [ trashes-clause-seq ] [ calls-clause-seq ]
        | trashes-clause-seq [ calls-clause-seq ]
        | calls-clause-seq
ensures-clause-seq ::= ensures-clause [ ensures-clause ] ...
ensures-clause ::= ensures [ redundantly ] post-cond ;
         | ensures [ redundantly ] liberally post-cond ;
post-cond ::= predicate

The behavior of a function is specified in the fun-spec-body, which consists of either the keyword behavior and several parts enclosed in a pair of braces ({ and }) or the keywords behavior program and a compound-statement. The first form is more abstract and preferable in situations where higher-order behavior is not required. See section 6.14 Behavior Programs for a discussion of the second form.

Although Larch/C++ has many parts available to specify the behavior of a C++ function, only a few are necessary in most cases. In this chapter, these simple cases are described first, and more complex variations later. Most of what you need to specify most functions in the behavior form is a single req-frame-ens, which can consist of an optional requires-clause (the precondition), an optional frame (that tells what can be modified, deallocated, or called), and an ensures-clause (the postcondition). To simplify things even further, we will postpone consideration of redundant clauses and the parts of the frame until later in the chapter.

The foundation of behavioral specification is the use of pre- and postconditions [Hoare69]. The precondition (pre-cond in the grammar) is a predicate that follows the Larch/C++ keyword requires. It specifies what is required of the client that calls the function. The postcondition (post-cond in the grammar) is a predicate that follows the Larch/C++ keyword ensures. It specifies what is ensured by the implementation of the function for calls that satisfy the precondition. The predicates are written with the vocabulary of the used trait or traits (see section 9 Specification Modules).

An example is the following. (An explanation follows.)

// @(#)$Id: isqrt.lh,v 1.8 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);
//@ }

An informal interpretation of this specification is that it specifies a C++ function named isqrt, which takes one int argument value, and returns an integer approximation to its square root. This function cannot throw any exceptions, because its interface is specified with the C++ syntax throw(). (See section 6.11 Exceptions for how to specify functions that can throw exceptions.)

In the behavioral part of the specification, the Larch/C++ keyword result stands for the result of a call. The formal argument x stands for the value of the argument. In the above example, the trait used is the built-in trait int (see section 11.1 Integer Types). This trait gives meaning to the trait functions used, including *, -, and +. The interface specified is that of a function named isqrt, which takes one int argument, and returns an int, and throws no exceptions. When one calls isqrt with argument x, if x is positive, then the result is some number that satisfies the postcondition. The postcondition has two disjuncts, separated by \/, which means "or" (see section 6.1.2 Logical Connectives). The first disjunct says that if the result squared is not less than x, then subtracting one from the result gives an approximation that is too small; hence the approximation returned may be larger than the true root, but not too large. Similarly, the second says that if the result squared is not greater than x, then adding one to the result gives an approximation that is too large.

As illustrated by the specification of isqrt, one can specify C++ functions that are not easily thought of as mathematical functions of their arguments. That is, a mathematical function, f, would be such that f(28) = f(28), but isqrt(28) might return, according to the specification, either 5 or 6, so that two calls isqrt(28) might give different results. For example, an implementation of isqrt that returned the larger of the two acceptable values every other time it was called would satisfy the above specification. (See section 6.9.1 Examples in Function Specifications for how to write such examples into the specification using the example-seq.)

Therefore it is better to think of a C++ function not as a mathematical function, but as a relation among its arguments and result. One can think of a relation as a set-valued function, so that such a relation is also a function from a (mathematical) tuple of argument (values) to a set of results. Viewed as a set-valued function, a relation has a domain, which is the set of all argument tuples for which the set of results is non-empty.

The precondition of a function specification (that does not use the keyword liberally) describes the argument values that are guaranteed to be related to some result. The postcondition describes the relation itself; that is, it describes the set of results that are related to the given arguments.

Still ignoring the keywords redundantly and liberally, the declaration-seq, and frame, a C++ function satisfies its specification if and only if for each type-correct function call, if the precondition predicate is satisfied by the arguments, then the function call terminates and the postcondition is satisfied by the result and the arguments. See section 6.2 Mutation for a more accurate definition that takes side-effects into account, including the declaration-seq and modifies-clause. See section 6.12 Liberal Specifications for a yet more accurate definition that takes non-termination (specified by the use of liberally) into account.

Note that if the precondition is not satisfied by the arguments of a call, nothing is said either about termination or about whether the postcondition is satisfied (if the function terminates). One way to interpret this is that client code should not call a function unless its precondition is satisfied.

The requires-clause-seq is optional; an omitted requires-clause-seq places no requirements on client code. Logically, an omitted requires-clause-seq is equivalent to a requires-clause-seq with one requires-clause of the following form.

requires true;

Either the frame or the ensures-clause-seq may be omitted, but not both. An omitted ensures-clause-seq is equivalent to stating that the function returns normally in a way that satisfies the frame. Logically, an omitted ensures-clause-seq is equivalent to a single ensures-clause of the following form.

ensures true;

An omitted frame is equivalent to a frame of the following form, which means that all objects may be accessed, no objects can be mutated, no objects may be trashed, and all functions may be called.

accesses everything;
modifies nothing;
trashes nothing;
calls everything;

(See section 6.5 The Accesses Clause for details on the accesses-clause-seq. See section 6.2 Mutation for details on the modifies-clause-seq. See section 6.3 Allocation and Deallocation for details on the trashes-clause-seq. See section 6.4 The Calls Clause for details on the calls-clause-seq.)

See section 6.9 Redundancy in Function Specifications for how to write optional examples into a specification, and for how to use the redundantly keyword. We call a clause redundant if it uses the redundantly keyword or if it is an example in an example-seq (see section 6.9.1 Examples in Function Specifications). All non-redundant clauses of a given kind at each level of a spec-case must precede all redundant clauses of that kind at that level. For example, one cannot put a redundant ensures-clause before a non-redundant one. Multiple non-redundant requires and ensures clauses act as if they were single clauses with their pre-conds or post-conds conjoined.

See section 6.10 Case Analysis for the meaning of a specification with multiple spec-cases. That section also describes the meaning of a spec-case with sub-cases.

See section 6.12 Liberal Specifications for the meaning of a specification that uses the keyword liberally.

The Larch/C++ keyword result can only be used in the postcondition. The sort of result is the sort associated with the return type specified for the function. In the above specification, result is of sort int. (See section 6.1.10 Larch/C++ Special Primaries for more details on the sort of result.)

The predicates in the pre- and postconditions principally use the following identifiers and keywords.

There are a few other specialized keywords that can be used in pre- and postconditions. These other keywords are described below, but the ones from the above list will suffice for simple specifications.

Arguments to functions in C++ are passed by value, so the sort of a formal parameter is not the same as the sort for an equivalent global variable declaration. However references have the same sorts. See section Sorts for Formal Parameters for more details and examples.

The following sections discuss function specifications in more detail.

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