=Paper=
{{Paper
|id=Vol-1186/paper-20
|storemode=property
|title=Certified Proofs in Programs Involving Exceptions
|pdfUrl=https://ceur-ws.org/Vol-1186/paper-20.pdf
|volume=Vol-1186
|dblpUrl=https://dblp.org/rec/conf/mkm/DumasDER14
}}
==Certified Proofs in Programs Involving Exceptions==
https://ceur-ws.org/Vol-1186/paper-20.pdf
Certified proofs in programs involving exceptions
Jean-Guillaume Dumas1 , Dominique Duval1 , Burak Ekici1 , and
Jean-Claude Reynaud2
1
Laboratoire J. Kuntzmann, Université de Grenoble. 51, rue des Mathématiques,
umr CNRS 5224, bp 53X, F38041 Grenoble, France,
{Jean-Guillaume.Dumas,Dominique.Duval,Burak.Ekici}@imag.fr.
2
Reynaud Consulting (RC), Jean-Claude.Reynaud@imag.fr.
Abstract. Exception handling is provided by most modern program-
ming languages. It allows to deal with anomalous or exceptional events
which require special processing. In computer algebra, exception han-
dling is an efficient way to implement the dynamic evaluation paradigm:
for instance, in linear algebra, dynamic evaluation can be used for ap-
plying programs which have been written for matrices with coefficients
in a field to matrices with coefficients in a ring. Thus, a proof system for
computer algebra should include a treatement of exceptions, which must
rely on a careful description of a semantics of exceptions. The categorical
notion of monad can be used for formalizing the raising of exceptions:
this has been proposed by Moggi and implemented in Haskell. In this pa-
per, we provide a proof system for exceptions which involves both raising
and handling, by extending Moggi’s approach. Moreover, the core part of
this proof system is dual to a proof system for side effects in imperative
languages, which relies on the categorical notion of comonad. Both proof
systems are implemented in the Coq proof assistant.
1 Introduction
Using exceptions is an efficient way to simultaneously compute with dynamic
evaluation in exact linear algebra. For instance, for computing the rank of a
matrix, a program written for matrices with coefficients in a field can easily be
modified by adding an exception treatment in order to be applied to a matrix
with coefficients in a ring: the exception mechanism provides an automatic case
distinction whenever it is required. The question that arises then is how to prove
correctness of the new algorithm. It would be nice to design proofs with two
levels, as we designed the algorithms: a first level without exceptions, then a
second level taking the exceptions into account. In this paper, we propose a
proof system following this principle.
Exceptions form a computational effect, in the sense that a syntactic expres-
sion f : X → Y is not always interpreted as a function Jf K : JXK → JY K (where,
as usual, the sets JXK and JY K denote the interpretations of the types X and
Y ). For instance a function which raises an exception can be interpreted as a
function Jf K : JXK → JY K + Exc where Exc is the set of exceptions and “+”
denotes the disjoint union. In a programming language, exceptions usually differ
from errors in the sense that it is possible to recover from an exception while this
is impossible for an error; thus, exceptions have to be both raised and handled.
The fundamental computational effect is the evolution of states in an im-
perative language, when seen from a functional point of view. There are several
frameworks for combining functional and imperative programming: the effect
systems classify the expressions according to the way they interact with the
store [11], while the Kleisli category of the monad of states (X × St)St (where
St is the set of states) also provides a classification of expressions [14]; indeed,
both approaches are related [20]. Lawvere theories were proposed for dealing
with the operations and equations related to computational effects [16,12]. An-
other related approach, based on the fact that the state is observed, relies on the
classification of expressions provided by the coKleisli category of the comonad
of states X × St and its associated Kleisli-on-coKleisli category [4].
The treatment of exceptions is another fundamental computational effect.
It can be studied from the point of view of the monad of exceptions X + Exc
(where Exc is the set of exceptions), or with a Lawvere theory, however in these
settings it is difficult to handle exceptions because this operation does not have
the required algebraicity property [17,18], in contrast with raising exceptions,
looking up and updating states. This makes exceptions much more difficult to
formalize than other effects in the Lawvere theory framework. This issue has
been circumvented in [19] in order to get a Hoare logic for exceptions, in [13] by
using both algebras and coalgebras and in [18] by introducing handlers. The for-
malization of exceptions can also be made from a coalgebraic point of view [10].
In this paper we extend Moggi’s original approach: we use the classification of
expressions provided by the Kleisli category of the monad of exceptions and its
associated coKleisli-on-Kleisli category; moreover, we use the duality between
states and exceptions discovered in [3]. However, it is not necessary to know
about monads or comonads for reading this paper: the definitions and results
are presented in an elementary way, in terms of equational theories.
In Section 2 we give a motivating example for the use of exceptions as an
efficient way to compute with dynamic evaluation in exact linear algebra. Then
in Section 3 we define the syntax of a simple language for dealing with exceptions.
The intended denotational semantics is described in Section 4: we dissociate the
core operations for switching between exceptions and non-exceptional values, on
one side, from their encapsulation in the raising and handling operations, on the
other side. In Section 5 we add decorations to the syntax, in order to classify the
expressions of the language according to their interaction with the exceptions.
Decorations extend the syntax much like compiler qualifiers or specifiers (e.g.,
like the throw annotation in C++ functions’ signatures). In addition, we also
decorate the equations, which provides a proof system for dealing with this
decorated syntax. The main result of the paper is that this proof system is sound
with respect to the semantics of exceptions (Theorem 1). A major property of
this new proof system is that we can separate the verification of the proofs in
two steps: a first step checks properties of the programs whenever there is no
effect, while a second step takes the effects into account via the decorations.
2
Several properties of exceptions have been proven using this proof system, and
these proofs have been verified in the Coq proof assistant.
2 Rank computations modulo composite numbers
Rank algorithms play a fundamental role in computer algebra. For instance,
computing homology groups of simplicial complexes reduces to computing ranks
and integer Smith normal forms of the associated boundary matrices [6]. One of
the most efficient method for computing the Smith normal form of such boundary
matrices also reduces to computing ranks but modulo the valence, a product
of the primes involved in the Smith form [7]. Now rank algorithms (mostly
Gaussian elimination and Krylov based methods) work well over fields (note
that Gaussian elimination can be adapted modulo powers of primes [7, §5.1]).
Modulo composite numbers, zero divisors arise. Gauss-Bareiss method could
be used but would require to know the determinant in advance, with is more
difficult than the valence. The strategy used in [7] is to factor the valence, but
only partially (factoring is still not polynomial). The large remaining composite
factors will have very few zero divisors and thus Gaussian elimination or Krylov
methods will have very few risks of falling upon them. Thus one can use dynamic
evaluation: try to launch the rank algorithm modulo this composite number with
large prime factors and “pretend” to be working over a field [8]. In any case,
if a zero divisor is encoutered, then the valence has been further factored (in
polynomial time!) and the algorithm can split its computation independently
modulo both factors. An effective algorithm design, here in C++, enabling this
dynamic evaluation with very little code modification, uses exceptions:
1. Add one exception at the arithmetic level, for signaling a tentative division
by a zero divisor, see Fig. 1.
inline Integer invmod(const Integer& a, const Integer& m) {
Integer gcd,u,v; ExtendedEuclideanAlgorithm(gcd,u,v,a,m);
if (gcd != 1) throw ZmzInvByZero(gcd);
return u>0?u:u+=m;
}
Fig. 1. Throwing an exception upon division by a non unit
2. Catch this exception inside the rank algorithm and throw a new exception
with the state of the rank iteration, see Fig. 2 (in our implementation the
class zmz wraps integers modulo m, the latter modulus being a static global
variable).
3. Then it is sufficient to wrap the rank algorithm with a dynamic evaluation,
splitting the continuation modulo both factors, see Fig. 3.
3
try {
invpiv = zmz(1) / A[k][k];
} catch (ZmzInvByZero e) {
throw GaussNonInvPivot(e.getGcd(), k, currentrank);
}
Fig. 2. Re-throwing an exception to forward rank and iteration number information
void DynEvalRank(RankPairs& vectranks, size t addedrank, ZmzMatrix& A) {
try {
long rank = gaussrank(A); // in place modifications of A
vectranks.push back(RankPair(rank+addedrank, zmz::getModulus()) );
} catch (GaussNonInvPivot e) { // Split
long mymodulus1 = zmz::getModulus()/e.getGcd();
long mymodulus2 = zmz::getModulus()/mymodulus1;
// Homomorphism on the (n-k)×(m-k) remaining block
zmz::setModulus( mymodulus1 );
ZmzMatrix M1(A,e.getIndex(),e.getIndex());
DynEvalRank(vectranks, e.getCurrentRank(), M1);
// Homomorphism on the (n-k)×(m-k) remaining block
zmz::setModulus( mymodulus2 );
ZmzMatrix M2(A,e.getIndex(),e.getIndex());
DynEvalRank(vectranks, e.getCurrentRank(), M2);
}}
Fig. 3. Recursive splitting wrapper around classical Gaussian elimination, packing a
list of pairs of rank and associated modulus.
The advantage of using exceptions over other software design is twofold: first,
throwing an exception at the arithmetic level and not only on the inverse call
in the rank algorithm allows to prevent that other unexpected divisions by zero
divisors go unnoticed; second, re-throwing a new exception in the rank algorithm
allows to keep its specifications unchanged. It also enables to keep the modifica-
tions of rank algorithms to a minimum and to clearly separate normal behavior
with primes from the exceptional handling of splitting composite moduli.
In the following, we propose a proof system with decorations, so that proofs
can easily be made in two steps: a first step without exceptions, that is, just
preserving an initial proof of the rank algorithm; then a second level taking the
exceptions into account.
4
3 Syntax for exceptions
The syntax for exceptions in computer languages depends on the language: the
keywords for raising exceptions may be either raise or throw, and for handling
exceptions they may be either handle, try-with, try-except or try-catch,
for instance. In this paper we rather use throw and try-catch. The syntax
for dealing with exceptions may be described in two parts: a basic part which
deals with the basic data types and an exceptional part for raising and handling
exceptions.
The language we develop is quite close to the Ynot language [15]. Like Ynot,
our approach is ”a generalization of the well-known ideas from type-and-effect
systems and their monadic counterparts”. However, we can use comonads as
well as monads, and we offer more modularity: in Ynot there is a single monad
encompassing all effects, while we are able to compose effects, thus enabling to
prove programs in several simpler stages.
The basic part of our syntax is a signature Sig base , made of types (or sorts)
and operations. The exceptional types form a subset T of the set of types of
Sig base . For instance in C++ any type (basic type or class) is an exceptional
type, while in Java there is a base class for exceptional types, such that the
exceptional types are precisely the subtypes of this base class. Now, we assume
that some basic signature Sig base and some set of exceptional types T have been
chosen.
The signature Sig exc for exceptions is made of Sig base together with the
operations for raising and handling exceptions, as follows.
Definition 1. The signature for exceptions Sig exc is made of Sig base with the
following operations: a raising operation for each exceptional type T and each
type Y :
throwT ,Y : T → Y ,
and a handling operation for each Sig exc -term f : X → Y , each non-empty list of
exceptional types (Ti )1≤i≤n and each family of Sig exc -terms (gi : Ti → Y )1≤i≤n :
try{f } catch {Ti ⇒ gi }1≤i≤n : X → Y .
An important, and somewhat surprising, feature of a language with excep-
tions is that all expressions in the language, including the try-catch expressions,
propagate exceptions. Indeed, if an exception is raised before some try-catch ex-
pression is evaluated, this exception is propagated. In fact, the catch block in a
try-catch expression may recover from exceptions which are raised inside the try
block, but the catch block alone is not an expression of the language. This means
that the operations for catching exceptions are private operations: they are not
part of the signature for exceptions. More precisely, the operations for raising
and handling exceptions can be expressed in terms of a private empty type and
two families of private operations: the tagging operations for creating exceptions
and the untagging operations for catching them (inside the catch block of any
try-catch expression). The tagging and untagging operations are called the core
5
operations for exceptions. They are not part of Sig exc , but the interpretations
of the operations for raising and handling exceptions, which are part of Sig exc ,
are defined in terms of the interpretations of the core operations. The meaning
of the core operations is given in Section 4.
Definition 2. Let Sig exc be the signature for exceptions. The core of Sig exc is
the signature Sig core made of Sig base with a type 0 called the empty type and
two operations for each exceptional type T :
tagT : T → 0 and untagT : 0 → T
where tagT is called the exception constructor or the tagging operation and
untagT is called the exception recovery or the untagging operation.
4 Denotational semantics for exceptions
In this Section we define a denotational semantics for exceptions which relies
on the common semantics of exceptions in various languages, for instance in
C++ [1, Ch. 15], Java [9, Ch. 14] or ML.
The basic part of the syntax is interpreted in the usual way: each type X is
interpreted as a set JXK and each operation f : X → Y of Sig base as a function
Jf K : JXK → JY K. But, when f : X → Y in Sig exc is a raising or handling
operation, or when f : X → Y in Sig core is a tagging or untagging operation, it
is not interpreted as a function Jf K : JXK → JY K: this corresponds to the fact that
the exceptions form a computational effect. The distinction between ordinary and
exceptional values is discussed in Subsection 4.1. Then, denotational semantics
of raising and handling exceptions are considered in Subsections 4.2 and 4.3,
respectively. We assume that some interpretation of Sig base has been chosen.
4.1 Ordinary values and exceptional values
In order to express the denotational semantics of exceptions, a fundamental point
is to distinguish between two kinds of values: the ordinary (or non-exceptional)
values and the exceptions. It follows that the operations may be classified ac-
cording to the way they may, or may not, interchange these two kinds of values:
an ordinary value may be tagged for constructing an exception, and later on the
tag may be cleared in order to recover the value; then we say that the exception
gets untagged. Let Exc be a set, called the set of exceptions. For each set A,
the set A + Exc is the disjoint union of A and Exc and the canonical inclusions
are denoted normal A : A → A + Exc and abrupt A : Exc → A + Exc. For each
functions f : A → B and g : Exc → B, we denote by [f |g] : A + Exc → B the
unique function such that [f |g] ◦ normal A = f and [f |g] ◦ abrupt A = g.
Definition 3. An element of A + Exc is an ordinary value if it is in A and an
exceptional value if it is in Exc. A function ϕ : A + Exc → B + Exc:
– raises an exception if there is some x ∈ A such that ϕ(x) ∈ Exc.
6
– recovers from an exception if there is some e ∈ Exc such that ϕ(e) ∈ B.
– propagates exceptions if ϕ(e) = e for every e ∈ Exc.
Clearly, a function ϕ : A + Exc → B + Exc which propagates exceptions may
raise an exception, but cannot recover from an exception. Such a function ϕ
is characterized by its restriction ϕ|A : A → B + Exc, since its restriction on
exceptions ϕ|Exc : Exc → B + Exc is the inclusion abrupt B of Exc in B + Exc.
In the denotational semantics for exceptions, we will see that a term f : X →
Y of Sig exc or Sig core may be interpreted either as a function Jf K : JXK → JY K or
as a function Jf K : JXK → JY K+Exc or as a function Jf K : JXK+Exc → JY K+Exc.
However, in all cases, it is possible to convert Jf K to a function from JXK + Exc
to JY K + Exc, as follows.
Definition 4. The upcasting conversions are the following transformations:
– every function ϕ : A → B gives rise to ϕ = normal B ◦ ϕ : A → B + Exc,
– every function ψ : A → B + Exc gives rise to Ţψ = [ψ|abrupt B ] : A + Exc →
B + Exc, which is equal to ψ on A and which propagates exceptions;
– it follows that every function ϕ : A → B gives rise to ϕ = Ţ( ϕ) =
[normal B ◦ ϕ|abrupt B ] = ϕ + id Exc : A + Exc → B + Exc, which is equal to
ϕ on A and which propagates exceptions.
Since the upcasting conversions are safe (i.e., injective), when there is no ambi-
guity the symbols , Ţ and may be omitted. In this way, for each f : X → Y
and g : Y → Z, whatever their effects, we get Jf K : JXK + Exc → JY K + Exc and
JgK : JY K+Exc → JZK+Exc, which can be composed. Thus, every term of Sig exc
and Sig core can be interpreted by first converting the interpretation of each of
its components f : X → Y to a function Jf K : JXK + Exc → JY K + Exc. For
Sig exc , this coincides with the Kleisli composition associated to the exception
monad A + Exc [14].
We will also use the following conversion.
Definition 5. The downcasting conversion is the following transformation:
– every function θ : A + Exc → B + Exc gives rise to Ťθ = θ ◦ normal A : A →
B + Exc which is equal to θ on A and which propagates exceptions.
This conversion is unsafe: different θ’s may give rise to the same Ťθ.
4.2 Tagging and raising exceptions
Raising exceptions relies on the interpretation of the tagging operations. The
interpretation of the empty type 0 is the empty set ∅; thus, for each type X the
interpretation of 0 + X can be identified with JXK.
Definition 6. Let Exc be the disjoint union of the sets JT K for all the exceptional
types T . Then, for each exceptional type T , the interpretation of the tagging
operation tagT : T → 0 is the coprojection function
JtagT K : JT K → Exc .
7
Thus, the tagging function JtagT K : JT K → Exc maps a non-exceptional value
(or parameter ) a ∈ JT K to an exception JtagT K(a) ∈ Exc. We can now define the
raising of exceptions in a programming language.
Definition 7. For each exceptional type T and each type Y , the interpretation
of the raising operation throwT ,Y is the tagging function JtagT K followed by the
inclusion of Exc in JY K + Exc:
JthrowT ,Y K = abrupt JY K ◦ JtagT K : JT K → JY K + Exc .
4.3 Untagging and handling exceptions
Handling exceptions relies on the interpretation of the untagging operations for
clearing the exception tags.
Definition 8. For each exceptional type T , the interpretation of the untagging
operation untagT : 0 → T is the function
JuntagT K : Exc → JT K + Exc ,
which satisfies for each exceptional type R:
(
normal JT K when R = T
JuntagT K ◦ JtagR K = : JRK → JT K + Exc.
abrupt JT K ◦ JtagR K when R 6= T
Thus, the untagging function JuntagT K, when applied to any exception e, first
tests whether e is in JT K; if this is the case, then it returns the parameter a ∈ JT K
such that e = JtagT K(a), otherwise it propagates the exception e. Since the do-
main of JuntagT K is Exc, JuntagT K is uniquely determined by its restrictions
to all the exceptional types, and therefore by the equalities in Definition 8. For
handling exceptions of types T1 , . . . Tn , raised by the interpretation of some term
f : X → Y of Sig exc , one provides for each i in {1, . . . , n} a term gi : Ti → Y
of Sig exc (thus, the interpretation of gi may itself raise exceptions). Then the
handling process builds a function which first executes f , and if f returns an ex-
ception then maybe catches this exception. The catching part encapsulates some
untagging functions, but the resulting function always propagates exceptions.
Definition 9. For each term f : X → Y of Sig exc , and each non-empty lists
(Ti )1≤i≤n of exceptional types and (gi : Ti → Y )1≤i≤n of terms of Sig exc , let
(recover i )1≤i≤n denote the family of functions defined recursively by:
(
[ Jgn K | abrupt Y ] ◦ untagTn when i = n
recover i = : Exc → Y + Exc
[ Jgi K | recover i+1 ] ◦ untagTi when i < n
Then the interpretation of the handling operation is:
Jtry{f } catch {Ti ⇒ gi }1≤i≤n K = [ normal Y | recover 1 ] ◦ Jf K.
8
It should be noted that Jf K : JXK → JY K + Exc and that similarly
Jtry{f } catch {Ti ⇒ gi }1≤i≤n K : JXK → JY K + Exc. When n = 1 we get:
Jtry{f } catch {T ⇒ g}K = [ normal Y | [ JgK | abrupt Y ] ◦ untagT ] ◦ Jf K .
This definition matches that of Java exceptions [9, Ch. 14] or C++ excep-
tions [1, §15]. In particular, in the interpretation of try{f } catch {Ti ⇒ gi }1≤i≤n ,
each function Jgi K may itself raise exceptions; and the types T1 , . . . , Tn need not
be pairwise distinct, but if Ti = Tj for some i < j then gj is never executed.
5 A decorated equational proof system for exceptions
In Sections 3 and 4 we have formalized the signature for exceptions Sig exc ,
its associated core signature Sig core , and we have described their denotational
semantics. However the soundness property is not satisfied, in the sense that the
denotational semantics is not a model of the signature, in the usual sense: indeed,
a term f : X → Y is not always interpreted as a function Jf K : JXK → JY K;
it may be interpreted as Jf K : JXK → JY K + Exc, or as Jf K : JXK + Exc →
JY K + Exc. In order to get soundness, in this Section we add decorations to the
signature for exceptions by classifying the operations and equations according
to the interaction of their interpretations with the mechanism of exceptions.
Signature
decoration / Decorated signature interpretation /
(sound) Semantics
(Section 3) (Section 5) (Section 4)
5.1 Decorations for exceptions
By looking at the interpretation (in Section 4) of the syntax for exceptions (from
Section 3), we get a classification of the operations and terms in three parts,
depending on their interaction with the exceptions mechanism. The terms are
decorated by (0), (1) and (2) used as superscripts, they are called respectively
pure terms, propagators and catchers, according to their interpretations:
(0) the interpretation of a pure term may neither raise exceptions nor recover
from exceptions,
(1) the interpretation of a propagator may raise exceptions but is not allowed
to recover from exceptions,
(2) the interpretation of a catcher may raise exceptions and recover from excep-
tions.
For instance, the decoration (0) corresponds to the decoration noexcept in C++
(replacement of the deprecated throw()) and the decoration (1) corresponds to
throw(...), still in C++. The decoration (2) is usually not encountered in the
language, since catching is the prerogative of the core untagging function, which
is private. Similarly, we introduce two kinds of equations between terms. This is
done by using two distinct relational symbols which correspond to two distinct
interpretations:
9
(≡) a strong equation is an equality of functions both on ordinary values and
on exceptions
(∼) a weak equation is an equality of functions only on ordinary values, but
maybe not on exceptions.
The interpretation of these three kinds of terms and two kinds of equations is
summarized in Fig. 4. It has been shown in Section 4.1 that any propagator can
be seen as a catcher and that any pure term can be seen as a propagator and
thus also as a catcher. This allows to compose terms of different nature, so that
it is not a restriction to give the interpretation of the decorated equations only
when both members are catchers.
Syntax Decorated syntax Interpretation
type type
X X JXK
term pure term
f (0)
X
f
/Y X /Y JXK
Jf K
/ JY K
term propagator
f (1)
X
f
/Y X /Y JXK
Jf K
/ JY K + Exc
term catcher
f (2)
X
f
/Y X /Y JXK + Exc
Jf K
/ JY K + Exc
equation strong equation
f = g : X → Y f (2) ≡ g (2) : X → Y Jf K = JgK
equation weak equation
f = g : X → Y f (2) ∼ g (2) : X → Y Jf K ◦ normal JXK = JgK ◦ normal JXK
Fig. 4. Interpretation of the decorated syntax.
Now we can add decorations to the signature for exceptions Sig exc and its
associated core signature Sig core , from Definitions 1 and 2.
Definition 10. The decorated signature for exceptions Sig deco exc and its asso-
ciated decorated core signature Sig deco
core are made of Sig exc and Sig core , respec-
tively, decorated as follows: the basic operations are pure, the tagging, raising and
handling operations are propagators, and the untagging operations are catchers.
5.2 Decorated rules for exceptions
In this Section we define an equational proof system for exceptions. This proof
system is made of the rules in Fig. 5. It can be used for proving properties of
10
exceptions, for instance in the Coq proof assistant. In Fig. 5, the decoration
properties are often grouped with other properties: for instance, “f (1) ∼ g (1) ”
means “f (1) and g (1) and f ∼ g”; in addition, the decoration (2) is usually
dropped, since the rules assert that every term can be seen as a catcher; and
several rules with the same premisses may be grouped together: H 1 ...Hn
C1 ...Cp stands
for H1C...H
1
n
,. . . , H1C...H
p
n
.
Rules (a) are the usual rules for the monadic equational logic; they are valid
for all decorated terms and for strong equations. Rules (b) provide more infor-
mation on the decorated monadic equational logic for exceptions; in particular,
the substitution of f in a weak equation g1 ∼ g2 holds only when f is pure,
which is quite restrictive. Rules (c) ensure that the empty type is a kind of ini-
tial type with respect to weak equations. Rules (d) are used for case distinctions
between exceptional arguments (on the “0” side of X + 0) and non-exceptional
arguments (on the “X” side of X + 0). The symbol Ť in rules (e) is interpreted
as the downcast conversion, see Definition 5. Rules in (f) mean that the tagging
operations are interpreted as the canonical inclusions of the exceptional types in
the set Exc, see Definition 6. The rules in (g) determine the untagging operations
up to strong equations: an untagging operation recovers the exception param-
eter whenever the exception type is matched, and it propagates the exception
otherwise see Definition 8.
Remark 1. It has been shown in [3] that the denotational semantics of the core
language for exceptions is dual to the denotational semantics for states: the
tagging and untagging operations are respectively dual to the lookup and update
operations. In fact, this duality is also valid for the decorated equational logics.
This decorated proof system is used now (in Definition 12) for construct-
ing the raising and handling operations from the core tagging and untagging
operations. It has to be noted that the term catch {Ti ⇒ gi }1≤i≤n ◦ f may
catch exceptions, while the handling operation, which coincides with catch {Ti ⇒
gi }1≤i≤n ◦ f on non-exceptional values, must propagate exceptions; this is why
the downcast operator Ť is used.
Definition 11. For each exceptional type T and each type Y , the raising oper-
(1)
ation throwT ,Y : T → Y is the propagator defined as:
(1)
throwT ,Y = [ ]Y ◦ tagT .
Definition 12. For each propagator f (1) : X → Y , each non-empty lists of types
(1) (2)
(Ti )1≤i≤n and propagators (gi : Ti → Y )1≤i≤n , let catch {Ti ⇒ gi }1≤i≤n : Y →
Y denote the catcher defined by:
(2)
catch {Ti ⇒ gi }1≤i≤n = [ id Y | recover 1 ]
11
(a) Monadic equational rules for exceptions (first part):
f :X→Y g:Y →Z X f f ≡g f ≡g g≡h
g◦f :X →Z id X : X → X f ≡f g≡f f ≡h
f : X → Y g1 ≡ g2 : Y → Z f1 ≡ f2 : X → Y g : Y → Z
g1 ◦ f ≡ g2 ◦ f : X → Z g ◦ f1 ≡ g ◦ f2 : X → Z
f :X→Y g:Y →Z h:Z→W f :X→Y f :X→Y
h ◦ (g ◦ f ) ≡ (h ◦ g) ◦ f f ◦ id X ≡ f id Y ◦ f ≡ f
(b) Monadic equational rules for exceptions (second part):
f (0) f (1) X f (0) g (0) f (1) g (1) f (1) ∼ g (1) f ≡g
f (1) f (2) (0)
id X (g ◦ f )(0) (g ◦ f )(1) f ≡g f ∼g
f f ∼g f ∼g g∼h
f ∼f g∼f f ∼h
f (0) : X → Y g1 ∼ g2 : Y → Z f1 ∼ f2 : X → Y g : Y → Z
g1 ◦ f ∼ g2 ◦ f g ◦ f1 ∼ g ◦ f2
X f, g : 0 → Y
(c) Rules for the empty type 0: (0)
[ ]X : 0 → X f ∼g
(d) Case distinction with respect to X + 0:
g (1) : X → Y k(2) : 0 → Y
[g | k](2) : X → Y [g | k] ∼ g [g | k] ◦ [ ]X ≡ k
f, g : X → Y f ∼ g f ◦ [ ] X ≡ g ◦ [ ]X
f ≡g
k(2) : X → Y
(e) Propagating exceptions:
(Ťk)(1) : X → Y Ťk ∼ k
(f) Tagging:
(1)
T ∈T (fT : T → Y )T ∈T
(1) (2)
tagT : T → 0 [fT ]T ∈T : 0 → Y [fT ]T ∈T ◦ tagT ∼ fT
f, g : 0 → Y f ◦ tagT ∼ g ◦ tagT for all T ∈ T
f ≡g
(g) Untagging:
T ∈T R, T ∈ T R 6= T
(2)
untagT : 0 → T untagT ◦ tagT ∼ id T untagT ◦ tagR ∼ [ ]T ◦ tagR
Fig. 5. Decorated rules for exceptions
12
(2)
where (recover i : 0 → Y )1≤i≤n denotes the family of catchers defined recur-
sively by:
(
(2) gn ◦ untagTn when i = n,
recover i =
[gi | recover i+1 ] ◦ untagTi when i < n.
Then, the handling operation (try{f } catch {Ti ⇒ gi }1≤i≤n )(1) : X → Y is the
propagator defined by:
try{f } catch {Ti ⇒ gi }1≤i≤n = Ť (catch {Ti ⇒ gi }1≤i≤n ◦ f )
When n = 1 we get:
try{f } catch {T ⇒ g} = Ť (catch {T ⇒ g} ◦ f ) = Ť ([ id Y | g ◦ untagT ] ◦ f ).
Now Theorem 1 derives easily, by induction, from Fig. 5 and 4 and from
Definitions 11 and 12.
Theorem 1. The decorated rules for exceptions and the raising and handling
constructions are sound with respect to the denotational semantics of exceptions.
5.3 A decorated proof: a propagator propagates
With these tools, it is now possible to prove properties of programs involving
exceptions and to check these proofs in Coq. For instance, let us prove that
given an exception, a propagator will do nothing apart from propagating it.
Recall that the interpretation of [ ]Z (or, more precisely, of [ ]Z ) is abrupt JZK :
Exc → JZK + Exc.
Lemma 1. For each propagator g (1) : X → Y we have g ◦ [ ]X ≡ [ ]Y .
Proof. This lemma can be proved as follows; the labels refer to Fig. 5, and their
subscripts to the proof in Coq of Fig. 6.
(c)3 X
(c)1 X (0)
[ ]X : 0 → X g:X→Y [ ]X Y
(a) (b)1 (c)4 (0)
(1)
g ◦ [ ]X : 0 → Y g (1) [ ]X [ ]Y
(c)2 (b)2 (b)3 (1)
g ◦ [ ]X ∼ [ ]Y (g ◦ [ ]X )(1) [ ]Y
(b)4
g ◦ [ ]X ≡ [ ]Y
The proof in Coq follows the same line as the mathematical proof above. It goes
as in Figure 6. The Coq library for exceptions, EXCEPTIONS-0.1.tar.gz, can
be found online: http://coqeffects.forge.imag.fr (in file Proofs.v) with proofs of
many other properties of programs involving exceptions.
It should be recalled that any Coq proof is read from bottom up. The
application of the from empty is weakly unique rule certifies that the term
g o (@empty X), because its domain is the empty type, is weakly equal to
the term (@empty Y). Thus, we have the left side sub-proof: g o (@empty
X) ∼ (@empty Y). There, weak equality is converted into strong: apply-
ing propagator weakeq is strongeq resolves the goal: g o (@empty X) ==
(@empty Y) and produces as sub-goals that there is no catcher involved in both
hand sides (middle and right side sub-proofs).
13
Lemma propagator propagates 1:
forall X Y (g: term Y X),
is propagator g -> g o (@empty X) == (@empty Y).
Proof.
intros.
(* (b)4 *) apply propagator weakeq is strongeq.
(* (b)2 *) apply is comp. assumption.
(* (b)1 *) apply is pure propagator. (* (c)3 *) apply is empty.
(* (b)3 *) apply is pure propagator. (* (c)4 *) apply is empty.
(* (c)2 *) apply from empty is weakly unique.
Qed.
Fig. 6. Proof in Coq that “a propagator propagates exceptions”
5.4 A hierarchy of exceptional types
In object-oriented languages, exceptions are usually the objects of classes which
are related by a hierarchy of subclasses. Our framework can be extended in
this direction by introducing a hierarchy of exceptional types: the set T is
endowed with a partial order _ called the subtyping relation, and the sig-
nature Sig base is extended with a cast operation castR,T : R → T whenever
R _ T . The interpretation of castR,T is a pure function JcastR,T K : JRK → JT K,
such that JcastT ,T K is the identity on JT K and when S _ R _ T then
JcastS ,T K = JcastR,T K ◦ JcastS ,R K. Definition 8 has to be modified as follows:
the function JuntagT K : Exc → JT K + Exc satisfies for each exceptional type R:
(
normal JT K ◦ JcastR,T K when R _ T
JuntagT K◦JtagR K = : JRK → JT K+Exc.
abrupt JT K ◦ JtagR K otherwise
6 Conclusion
Exceptions are part of most modern programming languages and they are useful
in computer algebra, typically for implementing dynamic evaluation. We have
presented a new framework for formalizing the treatment of exceptions. These
decorations form a bridge between the syntax and the denotational semantics
by turning the syntax sound with respect to the semantics, without adding any
explicit “type of exceptions” as a possible return type for the operations. The
salient features of our approach are:
– We provide rules for equational proofs on programs involving exceptions
(Fig. 5) and an automatic process for interpreting these proofs (Fig. 4).
– Decorating the equations allows to separate properties that are true only up
to effects (weak equations) from properties that are true even when effects
are considered (strong equations).
14
– Moreover, the verification of the proofs can be done in two steps: in a first
step, decorations are dropped and the proof is checked syntactically; in a sec-
ond step, the decorations are taken into account in order to prove properties
involving computational effects.
– The distinction between the language for exceptions and its associated pri-
vate core language (Definitions 1 and 2) allows to split the proofs in two
successive parts; in addition, the private part can be directly dualized from
the proofs on global states (relying on [3] and [4]).
– A proof assistant can be used for checking the decorated proofs on ex-
ceptions. Indeed the decorated proof system for states, as described in [4]
has been implemented in Coq [2] and dualized for exceptions (see http:
//coqeffects.forge.imag.fr).
We have used the approach of decorated logic, which provides rules for com-
putational effects by adding decorations to usual rules for “pure” programs.
This approach can be extended in order to deal with multivariate operations [5],
conditionals, loops, and high-order functions.
References
1. Working Draft, Standard for Programming Language C++. ISO/IEC
JTC1/SC22/WG21 standard 14882:2011.
2. Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous. Formal
verification in Coq of program properties involving the global state effect. JFLA’13,
Fréjus, France, 2013. arXiv:1310.0794.
3. Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse, Jean-Claude Reynaud.
A duality between exceptions and states. Mathematical Structures in Computer
Science 22, p. 719-722 (2012).
4. Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse, Jean-Claude Reynaud.
Decorated proofs for computational effects: States. ACCAT 2012. Electronic Pro-
ceedings in Theoretical Computer Science 93, p. 45-59 (2012).
5. Jean-Guillaume Dumas, Dominique Duval, Jean-Claude Reynaud. Cartesian effect
categories are Freyd-categories. Journal of Symbolic Computation 46, p. 272-293
(2011).
6. Jean-Guillaume Dumas, Frank Heckenbach, B. David Saunders, and Volkmar
Welker. Computing simplicial homology based on efficient Smith normal form
algorithms. In Michael Joswig and Nobuki Takayama, editors, Algebra, Geometry
and Software Systems, pages 177–206. Springer, March 2003.
7. Jean-Guillaume Dumas, B. David Saunders, and Gilles Villard. On efficient sparse
integer matrix Smith normal form computations. Journal of Symbolic Computa-
tion, 32(1/2):71–99, July–August 2001.
8. Dominique Duval. Simultaneous computations in fields of different characteristics.
In Erich Kaltofen and Stephen M. Watt, editors, Computers and Mathematics,
pages 321–326. Springer US, 1989.
9. James Gosling, Bill Joy, Guy Steele, Gilad Bracha. The Java Language Specifica-
tion, Third Edition. Addison-Wesley Longman (2005).
10. Bart Jacobs. A Formalisation of Java’s Exception Mechanism. ESOP 2001.
Springer Lecture Notes in Computer Science 2028. p. 284-301 (2001).
15
11. John M. Lucassen, David K. Gifford. Polymorphic effect systems. POPL 1988.
ACM Press, p. 47-57.
12. Martin Hyland, John Power. The Category Theoretic Understanding of Universal
Algebra: Lawvere Theories and Monads. Electronic Notes in Theoretical Computer
Science 172, p. 437-458 (2007).
13. Paul Blain Levy. Monads and adjunctions for global exceptions. MFPS 2006. Elec-
tronic Notes in Theoretical Computer Science 158, p. 261-287 (2006).
14. Eugenio Moggi. Notions of Computation and Monads. Information and Computa-
tion 93(1), p. 55-92 (1991).
15. Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars
Birkedal. Ynot: Dependent Types for Imperative Programs. Proceedings of the
13th ACM SIGPLAN International Conference on Functional Programming (ICFP
’08), p. 229-240 (2008).
16. Gordon D. Plotkin, John Power. Notions of Computation Determine Monads. FoS-
SaCS 2002. Springer-Verlag Lecture Notes in Computer Science 2303, p. 342-356
(2002).
17. Gordon D. Plotkin, John Power. Algebraic Operations and Generic Effects. Applied
Categorical Structures 11(1), p. 69-94 (2003).
18. Gordon D. Plotkin, Matija Pretnar. Handlers of Algebraic Effects. ESOP 2009.
Springer-Verlag Lecture Notes in Computer Science 5502, p. 80-94 (2009).
19. Lutz Schröder, Till Mossakowski. Generic Exception Handling and the Java
Monad. AMAST 2004. Springer-Verlag Lecture Notes in Computer Science 3116,
p. 443-459 (2004).
20. Philip Wadler. The Marriage of Effects and Monads. ICFP 1998. ACM Press,
p. 63-74 (1998).
16