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 programcompound-statement uses-seq ::= uses-clause [ uses-clause ] ... spec-case-seq ::= spec-case [alsospec-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]liberallypost-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.
result (in the postcondition),
this, self, and the names of appropriately scoped data
members can be used in the specification of a member
function (see section 7 Class Specifications).
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 6.1.8.1 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.