Jean-Guillaume Dumas
email: jean-guillaume.dumas@imag.fr.

Dominique Duval
email: dominique.duval@imag.fr.

Burak Ekici
email: burak.ekici@imag.fr.

Jean-Claude Reynaud
email: claude.reynaud@imag.fr.

Certified proofs in programs involving exceptions

Exception handling is provided by most modern programming languages. It allows to deal with anomalous or exceptional events which require special processing. In computer algebra, exception handling is an efficient way to implement the dynamic evaluation paradigm: for instance, in linear algebra, dynamic evaluation can be used for applying 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 paper, 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.

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 expression f : X → Y is not always interpreted as a function f : X → Y (where, as usual, the sets X and Y denote the interpretations of the types X and Y ). For instance a function which raises an exception can be interpreted as a function f : X → Y + 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 imperative 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 [START_REF] Lucassen | Polymorphic effect systems[END_REF], 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 [START_REF] Moggi | Notions of Computation and Monads[END_REF]; indeed, both approaches are related [START_REF] Wadler | The Marriage of Effects and Monads[END_REF]. Lawvere theories were proposed for dealing with the operations and equations related to computational effects [START_REF] Plotkin | Notions of Computation Determine Monads[END_REF][START_REF] Hyland | The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads[END_REF]. Another related approach, based on the fact that the state is observed, relies on the classification of expressions provided by the coKleisli category of comonad of states X × St and its associated Kleisli-on-coKleisli category [START_REF] Dumas | Decorated proofs for computational effects: States[END_REF].

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 [START_REF] Plotkin | Algebraic Operations and Generic Effects[END_REF][START_REF] Plotkin | Handlers of Algebraic Effects[END_REF]. This issue has been circumvented in [START_REF] Schröder | Generic Exception Handling and the Java Monad[END_REF] in order to get a Hoare logic for exceptions, in [START_REF] Blain | Monads and adjunctions for global exceptions[END_REF] by using both algebras and coalgebras. and in [START_REF] Plotkin | Handlers of Algebraic Effects[END_REF] by introducing handlers. The formalization of exceptions can also be made from a coalgebraic point of view [START_REF] Jacobs | A Formalisation of Java's Exception Mechanism[END_REF]. 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 [START_REF] Dumas | A duality between exceptions and states[END_REF]. 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 ex-pressions 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 5.5). 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. Several properties of exceptions have been proven using this proof system, and these proofs have been verified in the Coq proof assistant.

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 [START_REF] Dumas | Computing simplicial homology based on efficient Smith normal form algorithms[END_REF]. 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 [START_REF] Dumas | On efficient sparse integer matrix Smith normal form computations[END_REF]. 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 [START_REF] Dumas | On efficient sparse integer matrix Smith normal form computations[END_REF] 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 [START_REF] Duval | Simultaneous computations in fields of different characteristics[END_REF]. 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. 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 modifications 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.

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 basic part of the syntax is a signature Sig base , made of a 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 3.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 : throw T ,Y : T → Y , and a handling operation for each Sig exc -term f : X → Y , each non-empty list of exceptional types (T i ) 1≤i≤n and each family of Sig exc -terms (g i :

T i → Y ) 1≤i≤n : try{f } catch {T i ⇒ g i } 1≤i≤n : X → Y .
An important, and somewhat surprising, feature of a language with exceptions is that all expressions in the language, including the try-catch expressions, propagate exceptions. Indeed, if an exception is raised before some try-catch expression 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 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 3.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 : tag T : T → 0 and untag T : 0 → T where tag T is called the exception constructor or the tagging operation and untag T is called the exception recovery or the untagging operation.

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++ [START_REF]Standard for Programming Language C++[END_REF]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 X and each operation f : X → Y of Sig base as a function f : X → Y .

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 f : X → Y : 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.

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 according 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 : A function ϕ : A + Exc → B + Exc:

Exc → A + Exc.
• raises an exception if there is some x ∈ A such that ϕ(x) ∈ Exc.

• 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 f : X → Y or as a function f : X → Y +Exc or as a function f : X +Exc → Y +Exc. However, in all cases, it is possible to convert f to a function from X + Exc to Y + Exc, as follows.

Definition 4.2. 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 ambiguity the symbols , Ţ and ։ may be omitted. In this way, for each f : X → Y and g : Y → Z, whatever their effects, we get f : X + Exc → Y + Exc and g : Y + Exc → Z + 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 f :

X + Exc → Y + Exc.
For Sig exc , this coincides with the Kleisli composition associated to the exception monad A + Exc [START_REF] Moggi | Notions of Computation and Monads[END_REF].

We will also use the following conversion. This conversion is unsafe: different θ's may give rise to the same Ťθ.

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 X .

Definition 4.4. Let Exc be the disjoint union of the sets T for all the exceptional types T . Then, for each exceptional type T , the interpretation of the tagging operation tag T : T → 0 is the coprojection function

tag T : T → Exc .
Thus, the tagging function tag T : T → Exc maps a non-exceptional value (or parameter ) a ∈ T to an exception tag T (a) ∈ Exc.

We can now define the raising of exceptions in a programming language.

Untagging and handling exceptions

Handling exceptions relies on the interpretation of the untagging operations for clearing the exception tags.

Definition 4.6. For each exceptional type T , the interpretation of the untagging operation untag T : 0 → T is the function

untag T : Exc → T + Exc ,
which satisfies for each exceptional type R:

untag T • tag R = normal T when R = T abrupt T • tag R when R = T : R → T + Exc.
Thus, the untagging function untag T , when applied to any exception e, first tests whether e is in T ; if this is the case, then it returns the parameter a ∈ T such that e = tag T (a), otherwise it propagates the exception e.

Since the domain of untag T is Exc, untag T is uniquely determined by its restrictions to all the exceptional types, and therefore by the equalities in Definition 4.6.

For handling exceptions of types T 1 , . . . T n , raised by the interpretation of some term f : X → Y of Sig exc , one provides for each i in {1, . . . , n} a term g i : T i → Y of Sig exc (thus, the interpretation of g i may itself raise exceptions). Then the handling process builds a function which first executes f , and if f returns an exception then maybe catches this exception. The catching part encapsulates some untagging functions, but the resulting function always propagates exceptions. Definition 4.7. For each term f : X → Y of Sig exc , and each non-empty lists (T i ) 1≤i≤n of exceptional types and (g i : T i → Y ) 1≤i≤n of terms of Sig exc , let (recover i ) 1≤i≤n denote the family of functions defined recursively by:

recover i = [ g n | abrupt Y ] • untag Tn when i = n [ g i | recover i+1 ] • untag Ti when i < n : Exc → Y + Exc
Then the interpretation of the handling operation is:

try{f } catch {T i ⇒ g i } 1≤i≤n = [ normal Y | recover 1 ] • f .
It should be noted that f : X → Y + Exc and that similarly try{f } catch {T i ⇒ g i } 1≤i≤n : X → Y + Exc.

When n = 1 we get:

try{f } catch {T ⇒ g} = [ normal Y | [ g | abrupt Y ] • untag T ] • f .
This definition matches that of Java exceptions [START_REF] Gosling | The Java Language Specification, Third Edition[END_REF]Ch. 14] or C++ exceptions [1, §15].

In particular, in the interpretation of try{f } catch {T i ⇒ g i } 1≤i≤n , each function g i may itself raise exceptions;

and the types T 1 , . . . , T n need not be pairwise distinct, but if T i = T j for some i < j then g j is never executed.

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 f : X → Y ; it may be interpreted as f : X → Y + Exc, or as f :

X + Exc → Y + 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

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 exceptions.

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:

(≡) 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, Syntax Decorated syntax Interpretation type type so that it is not a restriction to give the interpretation of the decorated equations only when both members are catchers. Now we can add decorations to the signature for exceptions Sig exc and its associated core signature Sig core , from Definitions 3.1 and 3.2.

X X X term pure term X f / / Y X f (0) / / Y X f / / Y term propagator X f / / Y X f (1) / / Y X f / / Y + Exc term catcher X f / / Y X f (2) / / Y X + Exc f / / Y + Exc equation strong equation f = g : X → Y f (2) ≡ g (2) : X → Y f = g equation weak equation f = g : X → Y f (2) ∼ g (2) : X → Y f • normal X = g • normal X
Definition 5.1. The decorated signature for exceptions Sig deco exc and its associated decorated core signature Sig deco core are made of Sig exc and Sig core , respectively, decorated as follows: the basic operations are pure, the tagging, raising and handling operations are propagators, and the untagging operations are catchers.

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 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: H1...Hn C1...Cp stands for H1...Hn C1 ,. . . , H1...Hn Cp .

(a) Monadic equational rules for exceptions (first part):

f : X → Y g : Y → Z g • f : X → Z X id X : X → X f f ≡ f f ≡ g g ≡ f f ≡ g g ≡ h f ≡ h f : X → Y g 1 ≡ g 2 : Y → Z g 1 • f ≡ g 2 • f : X → Z f 1 ≡ f 2 : X → Y g : Y → Z g • f 1 ≡ g • f 2 : X → Z f : X → Y g : Y → Z h : Z → W h • (g • f ) ≡ (h • g) • f f : X → Y f • id X ≡ f f : X → Y id Y • f ≡ f (b)
Monadic equational rules for exceptions (second part):

f (0) f (1) f (1) f (2) X id (0) X f (0) g (0) (g • f ) (0) f (1) g (1) (g • f ) (1) f (1) ∼ g (1) f ≡ g f ≡ g f ∼ g f f ∼ f f ∼ g g ∼ f f ∼ g g ∼ h f ∼ h f (0) : X → Y g 1 ∼ g 2 : Y → Z g 1 • f ∼ g 2 • f f 1 ∼ f 2 : X → Y g : Y → Z g • f 1 ∼ g • f 2
(c) Rules for the empty type 0:

X [ ] (0)
X : 0 → X f, g : 0 → Y 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 (e)
Propagating exceptions: k (2) : X → Y (Ťk) (1) : X → Y Ťk ∼ k (f) Tagging: Rules (b) provide more information on the decorated monadic equational logic for exceptions; in particular, the substitution of f in a weak equation g 1 ∼ g 2 holds only when f is pure, which is quite restrictive.

T ∈ T tag (1) T : T → 0 (f (1) T : T → Y ) T ∈T [f T ] (2) T ∈T : 0 → Y [f T ] T ∈T • tag T ∼ f T f, g : 0 → Y f • tag T ∼ g • tag T for all T ∈ T f ≡ g (g) Untagging: T ∈ T untag (2)
T : 0 → T untag T • tag T ∼ id T R, T ∈ T R = T untag T • tag R ∼ [ ] T • tag R
Rules (c) ensure that the empty type is a kind of initial 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 4.3.

Rules in (f) mean that the tagging operations are interpreted as the canonical inclusions of the exceptional types in the set Exc, see Definition 4.4.

The rules in (g) determine the untagging operations up to strong equations: an untagging operation recovers the exception parameter whenever the exception type is matched, and it propagates the exception otherwise see Definition 4.6. Remark 5.2. It has been shown in [START_REF] Dumas | A duality between exceptions and states[END_REF] 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 5.4) for constructing the raising and handling operations from the core tagging and untagging operations. It has to be noted that the term catch {T i ⇒ g i } 1≤i≤n • f may catch exceptions, while the handling operation, which coincides with catch {T i ⇒ g i } 1≤i≤n • f on non-exceptional values, must propagate exceptions; this is why the downcast operator Ť is used.

T ,Y = [ ] Y • tag T .
Definition 5.4. For each propagator f (1) : X → Y , each non-empty lists of types (T i ) 1≤i≤n and propagators (g

(1) i : T i → Y ) 1≤i≤n , let catch {T i ⇒ g i } (2)
1≤i≤n : Y → Y denote the catcher defined by:

catch {T i ⇒ g i } (2) 1≤i≤n = [ id Y | recover 1 ]
where (recover (2) i : 0 → Y ) 1≤i≤n denotes the family of catchers defined recursively by: recover

(2) i = g n • untag Tn when i = n, [g i | recover i+1 ] • untag Ti when i < n.
Then, the handling operation (try{f } catch {T i ⇒ g i } 1≤i≤n ) (1) : X → Y is the propagator defined by:

try{f } catch {T i ⇒ g i } 1≤i≤n = Ť (catch {T i ⇒ g i } 1≤i≤n • f ) When n = 1 we get: try{f } catch {T ⇒ g} = Ť (catch {T ⇒ g} • f ) = Ť ([ id Y | g • untag T ] • f ).
Now Theorem 5.5 derives easily, by induction, from Fig. 5 and4 and from Definitions 5.3 and 5.4.

Theorem 5.5. The decorated rules for exceptions and the raising and handling constructions are sound with respect to the denotational semantics of exceptions.

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 Z : Exc → Z + Exc.
Lemma 5.6. 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.

X (c)1 [ ] X : 0 → X g : X → Y (a) g • [ ] X : 0 → Y (c)2 g • [ ] X ∼ [ ] Y g (1) X (c)3 [ ] (0) X (b)1 [ ] (1) X (b)2 (g • [ ] X ) (1) Y (c)4 [ ] (0) Y (b)3 [ ] (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. Last, 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: applying 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).

Lemma propagator propagates 1: forall X Y (g: term Y X), is propagator g -> g o (@empty X) == (@empty Y).

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 signature Sig base is extended with a cast operation cast R,T : R → T whenever R T . The interpretation of cast R,T is a pure function cast R,T : R → T , such that cast T ,T is the identity on T and when S R T then cast S ,T = cast R,T • cast S ,R . Definition 4.6 has to be modified as follows: the function untag T : Exc → T + Exc satisfies for each exceptional type R:

untag T • tag R = normal T • cast R,T when R T abrupt T • tag R otherwise : R → T +Exc.

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).

• 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 second 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 private core language (Definitions 3.1 and 3.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 [START_REF] Dumas | A duality between exceptions and states[END_REF] and [START_REF] Dumas | Decorated proofs for computational effects: States[END_REF]).

• A proof assistant can be used for checking the decorated proofs on exceptions. Indeed the decorated proof system for states, as described in [START_REF] Dumas | Decorated proofs for computational effects: States[END_REF] has been implemented in Coq [START_REF] Dumas | Formal verification in Coq of program properties involving the global state effect[END_REF] and dualized for exceptions (see http://coqeffects.forge.imag.fr).

Figure 2 :

 2 Figure 2: Re-throwing an exception to forward rank and iteration number information

voidFigure 3 :

 3 Figure 3: Recursive splitting wrapper around classical Gaussian elimination, packing a list of pairs of rank and associated modulus.

  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 4.1. An element of A + Exc is an ordinary value if it is in A and an exceptional value if it is in Exc.

Definition 4 . 3 .

 43 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.

Definition 4 . 5 .

 45 For each exceptional type T and each type Y , the interpretation of the raising operation throw T ,Y is the tagging function tag T followed by the inclusion of Exc in Y + Exc: throw T ,Y = abrupt Y • tag T : T → Y + Exc .

Figure 4 :

 4 Figure 4: Interpretation of the decorated syntax.

Figure 5 :

 5 Figure 5: Decorated rules for exceptions 12

Definition 5 . 3 .

 53 For each exceptional type T and each type Y , the raising operation throw (1) T ,Y : T → Y is the propagator defined as: throw (1)

  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.

Figure 6 :

 6 Figure 6: Proof in Coq that "a propagator propagates exceptions"

We have used the approach of decorated logic, which provides rules for computational 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 languages.


Christian Lévêque
email: christian.leveque@univ-amu.fr

Géraldine Ferracci

Yves Maulet

Chloé Grand-Masson

Marie-Pierre Blanchard

Michael Seagar

Oussama El Far

A substrate sensor chip to assay the enzymatic activity of Botulinum neurotoxin A

Keywords: BoNT, botulinum neurotoxin, SPR, surface plasmon resonance, RU, resonance unit, BSA, bovine serum albumin, LD 50 , median lethal dose, Hepes, 4-(2hydroxyethyl)-1-piperazine ethane sulfonic acid, SNAP-25, Synaptosomal-associated protein 25, DTT, Dithiothreitol, HBS, HEPES-buffered saline, LOD, limit of detection, LOQ, limit of quantification botulinum neurotoxin, SNAP-25, surface plasmon resonance, toxin sensor, endoprotease, neo-epitope

Botulinum neurotoxin A (BoNT/A) induces muscle paralysis by enzymatically cleaving the presynaptic SNARE protein SNAP-25, which results in lasting inhibition of acetylcholine release at the neuromuscular junction. A rapid and sensitive in vitro assay for BoNT/A is required to replace the mouse lethality assay (LD 50 ) in current use. We have developed a fully automated sensor to assay the endoprotease activity of BoNT/A. We produced monoclonal antibodies (mAbs) that recognize SNAP-25 neo-epitopes specifically generated by BoNT/A action. Recombinant SNAP-25 was coupled to the sensor surface of a surface plasmon resonance (SPR) system and samples containing BoNT/A were injected over the substrate sensor. On-line substrate cleavage was monitored by measuring binding of mAb10F12 to a SNAP-25 neo-epitope. The SNAP25-chip assay was toxin serotype-specific and detected 55 fM BoNT/A (1 LD 50 /ml) in 5 minutes and 0.4 fM (0.01 LD 50 /ml) in 5 hours.

Time-course and dose-response curves were linear, yielding a limit of quantification of 0.03 LD 50 /ml. This label-free method is 100 times more sensitive than the mouse assay, potentially providing rapid read-out of small amounts of toxin for environmental surveillance and the quality control of pharmaceutical preparations.

Introduction

Neurotoxins from Clostridium botulinum (BoNTs) act at the neuromuscular junction and cause the human disease botulism. BoNTs display endoprotease activity specific for the SNARE proteins that support Ca 2+ -dependent exocytosis at the nerve terminal. Thus, cleavage of SNAREs by BoNTs inhibits acetylcholine release and compromises muscle contraction. Most cases of botulism occur through ingestion of contaminated food, with the toxin reaching peripheral nerve terminals via the circulation. Although human botulism is relatively rare, the intoxicated patient needs prolonged and extensive clinical support to counteract descending flaccid paralysis, which can lead to death by respiratory failure if untreated.

Seven different BoNT-serotypes are known, but four (BoNT/A, B, E and F) predominate in human botulism. BoNT/A is the most frequent toxin serotype detected in human botulism in the USA [START_REF] Arnon | Botulinum toxin as a biological weapon: medical and public health management[END_REF]. It is also the most potent and can persist in an active form in neurons for weeks or months. BoNT/A was the first BoNT to be introduced for clinical use in the 1980s. Since then, its indications have expanded steadily and BoNT/A is currently used therapeutically to inhibit hyper-contraction or hyper-secretion in a large range of human diseases, as well as cosmetically to reduce facial wrinkles. Moreover BoNT/A is a class A agent that constitutes a potential biological weapon [START_REF] Dhaked | Botulinum toxin: bioweapon & magic drug[END_REF].

BoNT/A occurs naturally as a high molecular mass complex of up to 900 kDa, composed of the neurotoxin (150 kDa) and a set of non-toxic components of Clostridial origin. The neurotoxin has two polypeptide chains, linked by a single disulfide bond and non-covalent interactions. Each chain has a distinct function. In vivo the heavy chain (100 kDa) vectors the toxin to motoneuron nerve terminals, via recognition of a specific receptor (synaptic vesicle protein 2 or SV2, associated with gangliosides). Binding results in endocytosis of the toxin followed by translocation of the light chain into the cytoplasm, concomitant with disulfide bond reduction. The light chain (50 kDa) possesses zinc-dependent endopeptidase activity, which specifically cleaves 9 amino acids from the C-terminus of the SNARE protein SNAP-25 (synaptosome-associated protein of 25 kDa). SNAP-25, which is anchored at the cytoplasmic surface of the synaptic plasma membrane, is a key component of the synaptic vesicle fusion machinery [START_REF] Rossetto | Botulinum neurotoxins[END_REF].

The standard method, used currently for serological diagnosis of botulism, surveillance and quality control of batches during pharmaceutical production, is the mouse toxicity bioassay, which has a detection limit of 1 LD 50 /ml (10-20 pg BoNT/A). However this procedure is increasingly considered as unethical and furthermore is relatively slow (24-48 h), as the symptoms of botulism in the mouse can take several days to appear. Thus the mouse assay is poorly adapted to emergency situations requiring rapid diagnosis and appropriate treatment.

Numerous in vitro assays have been proposed as substitutes for the mouse lethality assay, and these fall into two main categories. The first only detects the neurotoxin protein using specific antibodies (ELISA-based predominantly), or the nucleic acids encoding it (PCR, immuno-PCR). The second includes the methods that assay BoNT/A biological activity (for reviews, [START_REF] Capek | Sensing the deadliest toxin: technologies for botulinum neurotoxin detection[END_REF][START_REF] Hakami | Gaining ground: assays for therapeutics against botulinum neurotoxin[END_REF][START_REF] Lindstrom | Laboratory diagnostics of botulism[END_REF] .

SPR is a powerful tool for studying biomolecular interactions. The versatility of SPR basedbiosensors extends beyond protein-protein interactions and environmental and medical applications are expanding [START_REF] Campbell | Use of a novel micro-fluidic device to create arrays for multiplex analysis of large and small molecular weight compounds by surface plasmon resonance[END_REF][START_REF] Helmerhorst | Real-time and Label-free Bio-sensing of Molecular Interactions by Surface Plasmon Resonance: A Laboratory Medicine Perspective[END_REF]. A few studies have used this label-free optical detection technique to measure protease activity using surface-captured substrate [START_REF] Loew | Proteolysis of the exodomain of recombinant protease-activated receptors: prediction of receptor activation or inactivation by MALDI mass spectrometry[END_REF][START_REF] Shoji | Real-time monitoring of matrix metalloproteinase-9 collagenolytic activity with a surface plasmon resonance biosensor[END_REF][START_REF] Steinrucke | Design of helical proteins for real-time endoprotease assays[END_REF].

However in all these reports, protease activity in the fluidic phase was monitored by a loss of substrate mass, leading to a decrease in SPR signal without revealing the site of cleavage.

In this report we describe a new simple and automated method to measure the enzymatic activity of BoNT/A entirely on-chip using SPR. On-chip cleavage of immobilized recombinant SNAP-25 was assayed by detecting neo-epitopes specific to BoNT/A endopeptidase activity. This provides a rapid and sensitive in vitro assay that quantifies BoNT/A activity on-line, by a gain-of-SPR signal.

Material and methods

2.1 Reagents: Amine coupling kits were from GE Healthcare and Biorad. ZnCl 2 , Tween 20, dithiothreitol (DTT), Fc specific goat anti-mouse IgG and fatty acid-free bovine serum albumin were from Sigma. Botulinum neurotoxins: frozen aliquots of BoNT/A (Metabiologics, USA) at 3.5 x 10 7 LD 50 /mg (1 mg/ml from Hall strain) or BoNT/B (Metabiologics, USA) at 1.1 x 10 7 LD 50 /ml (1 mg/ml from Okra strain) were used immediately after thawing. BoNT/E and C (provided by Prof. S Kozaki, Osaka Prefecture University) were produced and purified as previously described [START_REF] Ferracci | Synaptic vesicle chips to assay botulinum neurotoxins[END_REF]. BoNT/A concentrations are indicated as molarity or mouse LD 50 /ml. All experiments were performed in accordance with French and European guidelines for handling botulinum neurotoxin.

Monoclonal antibody production:

Mice were immunized with a synthetic peptide identical to the 191-197 sequence of rat SNAP-25. This sequence is located immediately N-terminal to the peptide bond cleaved by BoNT/A (Q 197 -R 198 ). A cysteine residue was added to the Nterminus of the peptide to allow coupling to KLH protein for immunization. Hybridomas were selected by ELISA against the coated peptide and for high affinity binding to SNAP-25 in plasma membrane vesicles treated with BoNT/A [START_REF] Marconi | A protein chip membrane-capture assay for botulinum neurotoxin activity[END_REF]. Monoclonal antibodies (mAb10F12) were purified by Protein A-Sepharose affinity chromatography and stored at -20°C.

Preparation of SNAP-25 chips:

Rat 6x His-SNAP-25 was cloned in pRSFDuet (Novagen).

His-SNAP-25 was expressed in BL21 and purified on Ni-NTA-agarose (Qiagen) beads under denaturing conditions according to the supplier's protocol and dialyzed against HBS (10 mM HEPES-NaOH pH 7.4, 150 mM NaCl). Purified proteins were stored in 20% glycerol at -80°C for a maximum of 6 months. SNAP-25 was amine coupled at pH 4.5 to Biacore CM5 (GE Healthcare) or pH 4 to ProteOn GLH (Biorad) sensor chips according to the manufacturer's instructions using automated programs. The final immobilization density was 9000 RU (CV = 4%, n= 15) on CM5 chips and 17000 RU (CV = 3.2%, n= 6 along a channel) on GLH chips, yielding a concentration of 10-30 µM. Chips were conditioned by injection of cleavage buffer (50 mM HEPES-NaOH pH 7.4, 0.1% BSA, 10 mM DTT, 1% Tween 20, 100 µM ZnCl 2, 10 mM DTT) and background signal was measured from five injections of mAb10F12 diluted in running buffer in the presence of anti-mouse Fc antibody, each at 10 µg/ml.

SPR analysis of

BoNT/A endoprotease activity: SPR measurements were performed at 34°C using Biacore 3000, Biacore T200 (GE Healthcare) or ProteOn XPR36 (Biorad) apparatuses with TBS (10 mM Tris-HCl pH 7.4, 150 mM NaCl ) or HBS as running buffer.

The minimum flow rates were 1 µl/min with the Biacore and 25 µl/min with the ProteOn apparatus. BoNT/A samples were serially diluted in cleavage buffer and placed in the sample rack at 4°C before injection. In all experiments, cleavage buffer in the absence of BoNT/A was injected onto a control lane coated with SNAP-25 (control flow cell or inter-spot area for Biacore or Biorad apparatus respectively). The pre-assembled mAb10F12/anti-mouse Fc antibody complex was then injected for 2 min over all flow cells. MAb binding was measured 10 sec after the end of injection, and the chip was regenerated with an 8 sec pulse of 10 mM glycine-HCl pH 2. The data obtained from the control flow cell were automatically subtracted from experimental measurements to yield the specific signal. The pre-assembled mAb10F12/anti-mouse Fc antibody complex yielded a 3-fold increase in detection sensitivity compared to mAb10F12 alone. Data were analyzed using Biaevaluation 4.1 software (Biacore/GEHeathcare) and ProteOn Manager v. 3.1.0.6 software (Biorad). Assuming a molecular weight ratio of 6:1 between mAb and SNAP-25 and that one mAb molecule binds to only one epitope at low rates of substrate cleavage, one RU of bound mAb10F12 corresponds to the cleavage of 0.015% of coupled substrate. The limit of detection (LOD) was measured in the absence of BoNT/A, and defined as the mean of the background plus three times the standard deviation. The limit of quantification (LOQ) was defined as the mean of the background plus ten times the standard deviation. SPR chips were used with at least 40 assay-regeneration cycles without significant loss of binding capacity. Chips were discarded when more than 10% of the substrate was cleaved.

Results

Production of monoclonal antibodies recognizing the reaction product of BoNT/A endopeptidase activity

The proteolytic activity of BoNT/A specifically cleaves a single peptide bond (Gln 197 -Arg 198 ) of SNAP-25, removing a nine residue (198-206) C-terminal fragment. In order to assay BoNT/A activity using a substrate chip, we produced antibodies designed to bind specifically the Cterminal neo-epitope of SNAP-25 1-197, generated by endopeptidase activity. Mouse monoclonal antibodies were raised against a synthetic peptide corresponding to residues 191-197 of SNAP-25 and screened by ELISA, Western blotting and SPR. Six positive hybridoma clones were obtained, producing mAbs which reacted with SNAP-25 in Western blots of rat brain membrane proteins treated with BoNT/A (Fig. 1a). These mAbs displayed no cross-reactivity with full-length SNAP-25 in untreated membranes. Clone 10F12 was selected for further study on the basis of its high affinity. The specificity of mAb10F12 for SNAP-25 cleaved by BoNT/A versus full length SNAP-25 was also confirmed by SPR experiments using the native protein in membrane fractions (Fig. 1b), as described in [START_REF] Marconi | A protein chip membrane-capture assay for botulinum neurotoxin activity[END_REF] and by immunocytochemical staining of cultured neurons incubated in the presence or absence of BoNT/A (Fig. S1).

Assay principle

Biosensors coupled to microfluidics flow cells work on the principle of continuous flow over a target coupled to the sensor surface. Samples are injected into the running buffer, at and for a given time. In this procedure, the target is the BoNT/A substrate, purified recombinant SNAP-25 immobilized on the reaction area called "flow cell" or "spot". The method incorporates two injection steps: (i) a cleavage step in which the sample containing BoNT/A is injected over the substrate. This clips off a nine residue C-terminal peptide and generates a neo-epitope specifically recognized by mAb10F12. (ii) A detection step in which mAb10F12 is injected. MAb10F12 binding to cleaved SNAP-25 produces an SPR signal in real time which is directly proportional to the amount of proteolytic product and thus to the concentration of BoNT/A in the initial sample (Fig. 2).

The duration of the sample injection step (ie. enzyme / substrate contact time) was varied between 5 and 300 min according to the BoNT/A concentration range to be assayed, whereas the detection step was set for 2 minutes. As the SPR signal generated is proportional to the molecular mass of bound molecules, mAb10F12 was pre-mixed with an anti-mouse Fc antibody to increase sensitivity.

Assay specificity

To confirm the specificity of BoNT/A activity detection, other BoNT serotypes were injected over SNAP-25 coated on a Biacore 3000 sensor chip at a relatively high concentrations (1 nM). No mAb10F12 binding signal was observed after BoNT/B injection (Fig. 3a), which cleaves the synaptic vesicle protein synaptobrevin / VAMP2. Similarly, BoNT/E and BoNT/C, which cleave SNAP-25 at different sites than BoNT/A [START_REF] Rossetto | Botulinum neurotoxins[END_REF], also failed to produce any signal (Fig. 3a). In contrast, injection of BoNT/A at a 1000-fold lower concentration (1 pM) generated a strong signal. These data indicate that the assay is specific for the endoprotease activity of BoNT/A, and qualifies this antibody to identify this serotype in an unknown sample.

Cumulative measurements of BoNT/A endoprotease activity

The SNAP-25 coupling procedure ensures that excess substrate (> 5 µM) is available.

Experiments were systematically carried out either with a low enzyme concentration, or with limited contact time, to ensure that less < 10% of substrate was cleaved. In these conditions, substrate concentration was considered to be constant during a single or a set of toxin injections in the same flow-cell. Signal repeatability, measured by at least 3 mAb injections, separated by acid regeneration of the sensor chip, was high (CV ~ 1% from 4 to 5000 RU, and 4% for 2 RU). Hence in principle several measurements can be performed in the same flow cell by monitoring successive increments in signal. Fig. 3b illustrates 7 consecutive injections of the same toxin concentration for 5 min, followed in each case by an independent mAb10F12 injection. Product formation over each 5 min period proceeds at a linear rate indicating that the reaction is not substrate-limited (Fig. 3c). At a fixed reference time this rate will depend linearly on enzyme concentration (see below).

Endoprotease activity were found to be independent of the buffer flow rate over the sensorchip between the limits of 1 and 25 µl/min (Fig. S2), indicating that diffusional transport of the enzyme to the solid-state substrate is non-limiting compared to the enzymatic reaction.

3.5: Rapid detection of BoNT/A activity

The rapidity of BoNT/A detection is of major importance in surveillance applications, thus the potential of SPR to achieve this aim was evaluated at 1 LD 50 /ml, a concentration that corresponds to the limit of detection for the in vivo mouse assay obtained in 24 h. In order to improve measurement sensitivity, experiments were carried out on a Biacore T200 apparatus which provides very low background. As illustrated in Fig. 4, specific endoprotease activity was readily detected after a 5 min injection of reduced BoNT/A, yielding 4.5 ± 1 RU (n=3), a value largely above the LOD (dashed line). Alternatively, non-reduced BoNT/A was diluted in cleavage buffer containing DTT and immediately injected. In these conditions, although all BoNT/A was not fully reduced and thus active, a cleavage time of 15 min was sufficient to clearly detect BoNT/A activity yielding 10.7 ± 1 RU (n=4, data not shown). These data indicate that our procedure provides a sensitivity of 1 LD 50 /ml (55 fM BoNT/A, i.e 1.3 pg of BoNT/A) within a time scale of 5-15 minutes injection.

Time-dependent sensitivity of the assay:

The dose-dependency of the method was evaluated using prolonged cleavage time with the multispot ProteOn biosensor. This device has a slightly lower sensitivity than the Biacore apparatus but has the advantage of allowing simultaneous injection of 6 samples over 6 different substrate-coated spots. This characteristic allows a direct comparison of SPR signals produced by different BoNT/A concentrations and dramatically increases the speed of sample analysis. Concentrations of BoNT/A ranging between 0.1 and 3 LD 50 /ml were injected 4 times each for a 15 min duration. Time course and dose-response curves were linear (Fig. S3 and Fig. 5a). 1 LD 50 / ml was detected in 15 min (Fig. 5a) and 0.1 LD 50 / ml in 1 hour (Fig. 5b). A linear dose-response relationship was also measured when BoNT/A (0.01 -0.3 LD 50 /ml) was injected for 5 h (Fig. 5c). In this case the LOD attained 0.01 LD 50 /ml (Fig. 5d) and the LOQ was 0.03 LD 50 /ml. Using a Biacore T200 the LOD was 0.03 LD 50 /ml (1.5 fM) and 0.008 LD 50 /ml (400 attomolar; 1 aM = 10 -18 M) for 1 and 5 hour injections respectively (data not shown).

Discussion

We have developed an SPR method to detect and assay the activity of botulinum neurotoxin A, one of the most potent neurotoxins in humans. This fully automated assay consists in injecting samples containing BoNT/A over a chip coated with substrate that can then be rapidly probed to measure the enzymatic product. BoNT/A cleaves a specific peptide bond, removing a six amino acid fragment and generating a new C-terminus. Production of a custom mAb directed against the C-terminal neo-epitope was thus crucial, as the specificity of the probe/analyte interaction determines an effective assay. Only two biological reagents, substrate and mAb10F12 are required to perform the assay and samples are directly analyzed with minimal handling. This assay is versatile as the contact time between BoNT/A and substrate can be modified depending on the purpose of the assay and the enzyme concentration to be determined. 1 LD 50 /ml (55 fM) was detected within a few minutes, in contrast to several hours required for the in vivo mouse assay. For applications in which extremely low concentrations of BoNT/A were to be detected, prolonging the cleavage time achieved a sensitivity of 0.008 LD 50 /ml (400 aM) in 5h. We predict that longer injection periods could attain even higher sensitivity in the attomolar range. A biosensor able to process simultaneous injections was used to generate linear dose response-curves for various contact times, demonstrating the potential of the method for quantitation down to 0.03 LD 50 /ml. Among the fastest tests for the detection of BoNT are those based on direct fluorescence measurement associated with substrate cleavage in solution. Although these assays are very appropriate for automated high-throughput screening of BoNT/A inhibitors, they lack sensitivity compared to the SPR assay: 1 nM BoNT/A detected in 2 minutes [START_REF] Schmidt | Fluorigenic substrates for the protease activities of botulinum neurotoxins, serotypes A, B, and F[END_REF], 4 pM detected in 120 min [START_REF] Poras | Detection and quantification of botulinum neurotoxin type a by a novel rapid in vitro fluorimetric assay[END_REF] versus 55 fM in 5 minutes for our assay. Although the SPR assay includes two steps: cleavage and detection, it can still compete with single-step assays in terms of rapidity, because detection is monitored on-line in the first few seconds, by a gain-of signal resulting from BoNT/A action.

The SPR procedure attains sensitivity similar to an optimized ELISA assay which constitutes to date the most sensitive enzymatic assay reported without prior concentration of BoNT/A [START_REF] Ekong | Recombinant SNAP-25 is an effective substrate for Clostridium botulinum type A toxin endopeptidase activity in vitro[END_REF][START_REF] Jones | The antinociceptive effects of botulinum toxin therapy for anal fissure are unproven[END_REF]. However, ELISA is a multistep, labor-intensive technique that requires long incubation periods. The automated SPR method offers several advantages over ELISA including shorter cleavage time (5 h versus 18 h) and detection time (minutes versus hours).

Several factors could contribute to the high sensitivity of the assay. Substrate immobilization on negatively charged hydrogels (dextran or alginate), that maintain SNAP-25 in an accessible conformation might accelerate enzymatic cleavage. Furthermore, as BoNT/A is positively charged at pH 7.4, it is possible that the negatively charged hydrogel concentrates the toxin and promotes its enzymatic activity in a similar way to negatively charged liposomes [START_REF] Caccin | VAMP/synaptobrevin cleavage by tetanus and botulinum neurotoxins is strongly enhanced by acidic liposomes[END_REF]. This kind of effect has been previously described for alphachymotrypsin acting on immobilized substrate [START_REF] Deere | Kinetics of enzyme attack on substrates covalently attached to solid surfaces: influence of spacer chain length, immobilized substrate surface concentration and surface charge[END_REF].

No loss of mass was detected during protease injection. This is due to the fact that only a small percentage of the substrate was cleaved and furthermore the released peptide (9 amino acids) accounts for only 4% of the total mass of SNAP-25. This procedure has several advantages over biosensor assays based on the measurement of mass loss upon enzymatic cleavage. Specific monitoring of the reaction product avoids false positives resulting from the action of other BoNT serotypes or non-specific proteolysis. Moreover it does not require coupling to other methods (eg. mass spectrometry) to analyze reaction products [START_REF] Henn | Catalytic enzyme activity on a biosensor chip: combination of surface plasmon resonance and mass spectrometry[END_REF]. Owing to the ratio of mAb/substrate mass and the fact that only few RU can be accurately measured, the method can in theory detect enzymatic cleavage of as low as 0.005% of the total immobilized substrate. This precision cannot be achieved by detecting loss of mass. Measurement of a minute amount of cleaved substrate authorizes multiple reuse of the sensor allowing us to monitor cleavage kinetics rather than a single end-point measurement or to repeat multiple assays on the same flow cell compatible with inhibitorscreening applications.

Conclusions

In conclusion this new biosensor method provides a simple, rapid and highly sensitive in vitro assay for the enzymatic activity of BoNT/A. SPR biosensors can operate in various media [START_REF] Ferracci | A label-free biosensor assay for botulinum neurotoxin B in food and human serum[END_REF] and the presence of BoNT/A could be detected in liquid foods using the method proposed. Alternatively the biosensor could be directly connected to a supply of drinking water and operate automatically to continuously monitor the presence of BoNT/A by repeatedly injecting the specific mAb at fixed times. In the future the method could be extended to detect all BoNTs that affect humans, providing antibodies that specifically recognize cleaved-substrates can be generated. Cleavage buffer in the presence or absence of 55 fM BoNT/A (1 LD 50 /ml) was injected over a SNAP-25 sensorchip (Biacore T200) for 5 minutes and cleavage products immediately detected using mAb10F12. Traces represent a typical experiment with superimposed signals generated by 3 injections of mAb10F12. Experiments in the absence of BoNT/A yielded a mean of -0.7 ± 0.4 RU (n = 7 independent experiments) and a LOD of 0.5 RU (dashed line). Cultured rat hippocampal neurons were prepared as described [START_REF] Ferracci | A label-free biosensor assay for botulinum neurotoxin B in food and human serum[END_REF]. Cells at 15 days in vitro were either untreated (control) or exposed to BoNT/A (1 nM) for 3 hours. BoNT/A (100 fM) was injected over surface-bound SNAP-25 (Biacore 3000) for 5 minutes at flow rates of 1, 5 or 25 µl/ml, followed by injection of mAb10F12. Representative of 3 independent experiments.

Fig. 1 :

 1 Fig. 1: Characterization of monoclonal antibodies designed to recognize the product of SNAP-25 cleavage by botulinum neurotoxin A.

Fig. 2 :

 2 Fig. 2: Assay for the endoprotease activity of botulinum neurotoxin A: general principle.

Fig. 3 :

 3 Fig. 3: Botulinum neurotoxin A: assay specificity and kinetics. a) Samples containing BoNT/A (1 pM), BoNT/B, BoNT/C, BoNT/E (all at 1 nM) or without BoNT (Cont.) were diluted in cleavage buffer and injected for 10 min over a SNAP-25 sensorchip. SNAP-25 cleavage was detected by injection of mAb10F12 (± SD, n= 3 mAb injections). Results are representative of 3 independent experiments. b) Seven successive injections of BoNT/A (200 fM) over immobilized SNAP-25 for a duration of 5 min. After each injection of toxin, mAb10F12 was injected and the amount of cleaved SNAP-25 measured 10 sec after the end of injection plotted in c).

Fig. 4 :

 4 Fig. 4: Rapid SPR detection of botulinum neurotoxin A at the mouse bioassay threshold.

Fig. 5 :

 5 Fig. 5: Multispot SPR analysis of botulinum neurotoxin A activity.

  Cells were then fixed for immunochemistry. SNAP-25 cleavage was detected using mAb10F12. Asterisk indicates soma localization. Scale bar = 20 m.

Fig. S2 :

 S2 Fig. S2: Influence of flow rate on protease activity.

Fig. S3 :

 S3 Fig.S3: Kinetics of botulinum neurotoxin A using a multispot biosensor.