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

6.11 Exceptions

As in C++, the interface of a function can declare what exceptions the function can throw (see Section r.15 in [Stroustrup91]). Note that the different exceptions that can be thrown are distinguished by their types. A common practice would be to define a class for each kind of exception; this class's data members could contain information pertinent to the exception. The following syntax is from C++.

exception-decl ::= throw ( [ type-list ] )
type-list ::= type-id [ , type-id ] ...

At run-time, a C++ function can either return or throw an exception, but not both. These two cases can be distinguished by using a lcpp-primary of the form returns or throws(type-id). These can only be used in a postcondition of an ensures-clause, or in an example.

In Larch/C++, both returning and throwing an exception is considered to be termination. Nontermination, of course, means going into an infinite loop. Nontermination also occurs when a function does not return to its caller, but jumps or exits or aborts in some fashion. See section 6.12.1 Terminates for more discussion on this point. Because both returning and throwing an exception is considered to be termination, they are both dealt with in the ensures-clause of a function specification.

The lcpp-primary returns is true when the function terminates and does not throw an exception. If the function terminates and ~returns is true, then some exception is raised.

A lcpp-primary of the form throws(T) is true when the function terminates and throws the exception T.

Formally, Larch/C++ models a function may throw an exception as a relation between pre-states pairs of tagged results and post-states. One can test the tags of such a tagged result using the primaries result and throws(T); one can extract the associated values with the primaries result and thrown(T). The primary result has a well-defined value when returns is true, and thrown(T) has a well-defined value when throws(T) is true.

See section 6.1.10 Larch/C++ Special Primaries for the syntax of a lcpp-primary beginning with thrown. The sort of an lcpp-primary of the form thrown(T) is the sort of a formal parameter of type T (see section Sorts for Formal Parameters). The sort an lcpp-primary of the form returns or throws(T) is bool.

The following is a simple example of a function specification with an exception specified. See section 6.10 Case Analysis for the meaning of having a global precondition and two subsidiary spec-cases.

// @(#)$Id: inc2.lh,v 1.17 1999/03/04 23:24:06 leavens Exp $

#include "Overflow.lh"

extern void inc2(int& i) throw(Overflow*);
//@ behavior {
//@   requires assigned(i, pre);
//@   {
//@      requires i^ + 2 <= INT_MAX;
//@      modifies i;
//@      ensures returns /\ i' = i^ + 2;
//@      ensures redundantly  result = theVoid;
//@    also
//@      requires i^ + 2 > INT_MAX;
//@      ensures throws(Overflow*);
//@      ensures redundantly  (*thrown(Overflow))' = theException;
//@   }
//@ }

In a specification of a function that can raise exceptions, it is important to use the returns and throws keywords to distinguish cases of the result. This is because the logic behind LSL will assign a value to result, even if returns is false! The above specification is a rather extreme example of this, as the set of abstract values for the type void contains only one element, theVoid (see section 11.5 void). Hence, writing result = theVoid in the postcondition is not equivalent to writing returns there; instead result = theVoid is equivalent to true [Jones95e]! Similarly, one cannot use thrown(Overflow) instead of throws(Overflow).

The above specification includes the following class specification, which is typical of how you would specify a class for an exception that contains no information. (See section 7 Class Specifications for the syntax and more details about class specifications.)

// @(#)$Id: Overflow.lh,v 1.7 1997/01/27 21:25:20 leavens Exp $

//@ uses NoInformationException(Overflow), NoContainedObjects(Overflow);
class Overflow { };

The trait used by the class overflow to describe its abstract values is built-in to Larch/C++ for specifying exceptions with no information. The abstract value of such an exception is thus named theException. It is the following trait. (The included trait is given below.)

% @(#) $Id: NoInformationException.lsl,v 1.2 1995/11/13 18:17:58 leavens Exp $
NoInformationException(T) : trait
  includes NoInformation(T, theException for it)

The above trait in turn includes the following trait, which specifies a one-point set.

% @(#) $Id: NoInformation.lsl,v 1.2 1995/11/13 18:18:58 leavens Exp $
NoInformation(T) : trait
  includes NoContainedObjects(T)
    it: -> T
  asserts T generated by it
    \forall x, y: T
      x == it;
      x == y;

One can also specify a function that can either throw an exception or do something else, without saying which. The following is an example. Note that this specification can be implemented by a function that always throws an exception.

// @(#)$Id: inc3.lh,v 1.11 1999/03/04 23:16:10 leavens Exp $

#include "Overflow.lh"

extern void inc3(int& i) throw(Overflow*);
//@ behavior {
//@   requires assigned(i, pre);
//@   modifies i;
//@   ensures (returns /\ i' = i^ + 3)
//@           \/ (throws(Overflow*) /\ unchanged(i));
//@   example i^ = 4 /\ i' = 7 /\ returns;
//@   example i^ = 4 /\ i' = 4 /\ throws(Overflow*);
//@ }

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