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 6.1.8.1 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)
introduces
it: -> T
asserts T generated by it
implies
\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.