Jean-Christophe Filliâtre

One Logic To Use Them All

Deductive program verication is making fast progress these days. One of the reasons is a tremendous improvement of theorem provers in the last two decades. This includes various kinds of automated theorem provers, such as ATP systems and SMT solvers, and interactive proof assistants. Yet most tools for program verication are built around a single theorem prover. Instead, we defend the idea that a collaborative use of several provers is a key to easier and faster verication. This paper introduces a logic that is designed to target a wide set of theorem provers. It is an extension of rst-order logic with polymorphism, algebraic data types, recursive denitions, and inductive predicates. It is implemented in the tool Why3, and has been successfully used in the verication of many non-trivial programs.

Introduction

The idea behind deductive program verication [START_REF] Filliâtre | Deductive software verication[END_REF] is to break down the correctness of a program to a set of logical formulas and to prove them valid. A tremendous improvement of theorem provers in the last two decades now allows this idea to scale up. Projects such as CompCert [START_REF] Leroy | A formally veried compiler back-end[END_REF] and seL4 [START_REF] Klein | seL4: Formal verication of an OS kernel[END_REF] show how interactive proof assistants (resp. Coq and Isabelle) can be successfully used to tackle large program verications. Even more impressive is the progress in automated provers 4 , notably the so-called SMT revolution. Designed with program verication in mind, SMT solvers have led to powerful verication tools, such as VCC [START_REF] Schulte | A glimpse of a verifying C compiler[END_REF], Frama-C [START_REF]The Frama-C platform for static analysis of C programs[END_REF], Dafny [START_REF] Leino | Dafny: An Automatic Program Verier for Functional Correctness[END_REF], or VeriFast [START_REF] Jacobs | The VeriFast program verier[END_REF], to mention only a few. Yet we note that most of these tools are built on top of a single automated prover (e.g. Z3 in the case of VCC, Dafny, or VeriFast) or a single dedicated prover to handle a specic program logic (e.g. B method [START_REF] Filliâtre | The B-Book, assigning programs to meaning[END_REF] or KIV [START_REF] Reif | Proving system correctness with KIV 3.0[END_REF]). We rather defend the idea that program verication should be done using as many theorem provers as possible, including those that were not necessarily designed with program verication in mind (e.g. ATP systems). We are developing the tool Why3 [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF][START_REF] Filliâtre | Why3 where programs meet provers[END_REF] to implement this idea. Both the specication logic of Why3 and its programming language, WhyML, are used as intermediate languages in tools such as Frama-C [START_REF]The Frama-C platform for static analysis of C programs[END_REF], Krakatoa [START_REF] Marché | The Krakatoa tool for certication of Java/JavaCard programs annotated in JML[END_REF], Easycrypt [START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF], and GNATprove [START_REF] Comar | Integrating formal program verication with testing[END_REF]. WhyML is also used directly to implement data structures and algorithms that can later be translated to executable OCaml code. Our gallery of veried programs (http://toccata.lri.fr/gallery/) currently contains more than 80 entries. These examples show the benets of our approach. Indeed, it is often the case that several theorem provers are successfully used in proving all goals, but none can prove all of them by itself. In particular, an interactive theorem prover can be used to discharge a complex lemma (for instance one requiring induction), while the remaining goals can all be discharged automatically.

Designing a logic to target a wide set of theorem provers is not that easy.

We have come up with a logic of compromise, that is not as rich as the logic of proof assistants such as Coq or PVS, yet richer than the usual logic of automated theorem provers. Our logic is an extension of rst-order logic with rank-1 polymorphism, algebraic data types, recursive denitions, and inductive predicates. The purpose of this paper is to dene this logic (Section 2), and to explain the processes by which Why3 translates it to the input format of fteen theorem provers (Section 3). Finally, Section 4 presents experimental results obtained in the context of program verication. We conclude with related work and perspectives.

A Polymorphic First-Order Logic

This section describes the logic of Why3 as faithfully as possible. Earlier work [START_REF] Bobot | Expressing Polymorphic Types in a Many-Sorted Language[END_REF] only describes the extension of rst-order logic with polymorphism. Here we also consider algebraic data types, recursive denitions, and inductive predicates.

Syntax

A type symbol is simply a name t and a type arity n ∈ N. We write it t α 1 , . . . , α n where the α i are type variables. Names α 1 , . . . , α n are not relevant but we adopt an homogeneous syntax for all symbols. We note d t such a declaration:

d t ::= t α, . .

. , α type symbol declaration

When n = 0, we say that t is a monomorphic type symbol and we simply write t instead of t . In the following, let Σ T be a set of type symbols. We assume that Σ T contains at least the two monomorphic type symbols int and real. Types are built from type variables and type symbols:

τ ::= α type variable | t τ, . . . , τ type symbol application
We note tv (τ ) the set of type variables of type τ . When tv (τ ) = ∅, we say that τ is a sort.

Function and predicate symbols are declared, possibly with polymorphic types, as follows: In the following, Σ F denotes a set of function symbols and Σ P a set of predicate symbols. We assume that Σ P contains at least a polymorphic predicate = α (α, α) that denotes equality. Terms and formulas are then built from function and predicate symbols according to the syntax given in Fig. 13. Note that syntax for terms and formulas are mutually recursive, since a conditional term expression if f then t 1 else t 2 involves a formula f . We note fv (t) (resp. fv (f ), fv (p)) the set of free variables of a term t (resp. a formula f , a pattern p). Denitions of fv (t) and fv (f ) are standard, variables being bound by let, quantiers, and patterns. A pattern p binds all variables in fv (p), which is dened as follows:

d f ::= f α, .
fv (x τ ) = {x τ } fv (f τ 1 , . . . , τ m (p 1 , . . . , p n )) = fv (p 1 ) ∪ • • • ∪ fv (p n ) fv ( ) = ∅ fv (p 1 | p 2 ) = fv (p 1 ) ∪ fv (p 2 ) fv (p as x τ ) = fv (p) ∪ {x τ }
The type checking rule for pattern p 1 | p 2 , given in next section, imposes that fv (p 1 ) and fv (p 2 ) are equal. Thus the denition above actually simplies to

fv (p 1 | p 2 ) = fv (p 1 ) = fv (p 2 ).
A signature Σ denotes a triple (Σ T , Σ F , Σ P ). A context Γ extends a signature Σ with denitions for some of its symbols. A denition d introduces either algebraic data types, recursive denitions, or inductive predicates, as follows: Example. Let Σ T be the following set of type symbols:

d ::= datatype
Σ T = {int, real, nat, list α , pair α 1 , α 2 }.
Let Σ F and Σ P be the following sets of function and predicate symbols: Here and below, we omit type annotations when they are obvious from the context.

Σ F = {O : nat, S (
| f ∧ f conjunction | f ∨ f disjunction | f ⇒ f implication | f ⇔ f equivalence | not f negation | true tautology | false absurdity | let xτ = t in f local binding | if f then f else f conditional expression | match t with p → f | . . . | p → f

Type Checking

For a signature Σ to be well-formed, any type expression τ occurring in a declaration of Σ F or Σ P must be well-typed, that is Σ τ . Additionally, the free type variables of τ must be included in the type variables α 1 , . . . , α m of the declaration. In the following, we only consider signatures that are well-formed.

Let Γ be a context extending a signature Σ with denitions. For Γ to be wellformed, any symbol from a denition must appear in Σ, and no symbol can be dened more that once. Type checking of types, terms, formulas, and patterns is straightforward. Judgements are Σ τ (type τ is well-formed in Σ), Σ t : τ (term t is wellformed and of type τ ), Σ f (formula f is well-formed), and Σ p : τ (pattern p is well-formed and of type τ ), respectively. Typing rules are given in Fig. 4 7. Note that, contrary to Hindley-Milner type system, the let binder does not generalize the type of the term that is bound. Thus polymorphism is introduced by symbols, but not by local denitions. In addition to these rules, we also check that, for any pattern matching expression match t with p 1 → . | . . . | p n → . end (in terms or formulas), t has type t τ 1 , . . . , τ m where type t is dened as an algebraic data type and patterns p 1 , . . . , p n cover any possible value for term t.

Finally, we perform the following checks on denitions.

Algebraic Data Types. Within a block of mutually-dened algebraic data types datatype a 1 with . . . with a k , each algebraic data type denition a i must have the form

t i α 1 , . . . , α m = f 1 α 1 , . . . , α m (. . . ) : t i α 1 , . . . , α m | . . . | f l α 1 , . . . , α m (. . . ) : t i α 1 , . . . , α m
that is, all constructors f j share the same type parameters as type t i and all have return type t i α 1 , . . . , α m . Additionally, we require that all types t i are inhabited according to the following denition: Type t i is inhabited if it has at least one constructor f j α 1 , . . . , α m (τ 1 , . . . , τ nj ) such that all types τ l are inhabited. Since types τ l may recursively involve types from data type denitions, such a denition is to be understood as a least xed point. Types from Σ that are not part of data type denitions are assumed to be inhabited. As a consequence of this denition, an algebraic data type must have at least one constructor. t α1, . . . , αm ∈ Σ Σ τi Σ t τ1, . . . , τm Fig. 4. Typing rule for types.

Σ c int : int Σ c real : real Σ τ Σ xτ : τ f α1, . . . , αm (τ 1 , . . . , τ n ) : τ ∈ Σ Σ τi σ = {α1 → τ1, . . . , αm → τm} Σ ti : σ(τ i ) Σ f τ1, . . . , τm (t1, . . . , tn) : σ(τ ) Σ t1 : τ Σ t2 : τ2 Σ let xτ = t1 in t2 : τ2 Σ f Σ t1 : τ Σ t2 : τ Σ if f then t1 else t2 : τ Σ t : t τ1, . . . , τm Σ pi : t τ1, . . . , τm Σ ti : τ Σ match t with p1 → t1 | . . . | pn → tn end : τ Fig. 5. Typing rules for terms. p α1, . . . , αm (τ 1 , . . . , τ n ) ∈ Σ Σ τi σ = {α1 → τ1, . . . , αm → τm} Σ ti : σ(τ i ) Σ p τ1, . . . , τm (t1, . . . , tn) Σ true Σ false Σ f1 Σ f2 • ∈ {∧, ∨, ⇒, ⇔} Σ f1 • f2 Σ τ Σ f Σ ∀xτ . f Σ τ Σ f Σ ∃xτ . f Σ f Σ not f Σ t : τ Σ f Σ let xτ = t in f Σ f1 Σ f2 Σ f3 Σ if f1 then f2 else f3
Σ t : t τ1, . . . , τm Σ pi : t τ1, . . . , τm Σ fi Σ match t with p1 → f1 | . . . | pn → fn end Fig. 6. Typing rules for formulas. Recursive Denitions.

Σ τ Σ xτ : τ Σ τ Σ : τ f α1, . . . , αm (τ 1 , . . . , τ n ) : τ ∈ Σ Σ τi σ = {α1 → τ1, . . . , αm → τm} i = j ⇒ fv (pi) ∩ fv (pj) = ∅ Σ pi : σ(τ i ) Σ f τ1, . . . , τm (p1, . . . , pn) : σ(τ ) fv (p1) = fv (p2) Σ pi : τ Σ p1 | p2 : τ xτ ∈ fv (p) Σ p : τ Σ p as xτ : τ
A block of mutually recursive denitions recursive δ 1 with . . . with δ k is well-formed if each denition δ i is well-typed. A function denition function f α, . . . , α (x τ , . . . , x τ ) : τ = t is well-typed if Σ t : τ , and a predicate denition predicate p α, . . . , α (x τ , . . . , x τ ) = f is well-typed if Σ f . Additionally, all free variables (including type variables) in t and f must belong to the symbol declaration. Finally, we require such denitions to terminate, according to the following criterion: there must exist a lexicographic order of arguments that guarantees a structural descent (over algebraic data types).

Inductive Predicates. An inductive denition

p α 1 , . . . , α m (τ 1 , . . . , τ n ) = f 1 | . . . |f k is well-formed if each clause f i is a closed formula, well-typed i.e. Σ f i , that
belongs to the following grammar:

f 0 ::= p α 1 , . . . , α m (t 1 , . . . , t n ) | f ⇒ f 0 | ∀x τ . f 0 | let x τ = t in f 0
Additionally, we require all inductive predicates from that block of inductive denitions to appear in strictly positive positions in the formulas on the left side of ⇒, so as to ensure the existence of a least xpoint.

In the following, we only consider contexts that are well-formed according to the typing rules we just introduced.

Semantics

We recall that a sort is a monomorphic type, that is, a type τ such that tv (τ ) = ∅. In the following, we use notation α (resp. s, x, t) for a vector of type variables (resp. sorts, variables, terms). Given a signature, a pre-interpretation [[.]] is dened as follows:

Each sort s is interpreted as a non-empty domain [[s]]. Sort int is interpreted as Z and sort real as R.

Given a function symbol f α (τ 1 , . . . , τ n ) : τ and sorts s, we interpret the instance f s as a function

[[f s ]] of type [[σ(τ 1 )]] × • • • × [[σ(τ n )]] → [[σ(τ )]]
where σ maps the type variables α to the sorts s.

Given a predicate symbol p α (τ 1 , . . . , τ n ) and sorts s, we interpret the instance p s as a function

[[p s ]] of type [[σ(τ 1 )]] × • • • × [[σ(τ n )]] → {⊥, }
where σ maps the type variables α to the sorts s. For each sort s, the predicate = s is interpreted as the equality over [[s]].

For any algebraic data type t α , with constructors f 1 α , . . . , f l α , we require [[t s ]] to be the free algebra generated by

[[f 1 s ]], . . . , [[f l s ]], that is for i = j, [[f i s ]](t) = [[f j s ]](u) (1)
[[f i s ]](t) = [[f i s ]](u) ⇒ t = u (2) ∀x ∈ [[t s ]], ∃i, ∃t, x = [[f i s ]](t) (3)
In the following, isf i denotes a predicate that identies values in [[t s ]] that are applications of f i , and projf i,j returns the j-th argument of such an application.

Given a pre-interpretation, a valuation v maps each type variable α to a sort v(α), and each variable x τ to some element of [[v(τ )]]. Given a pre-interpretation and a valuation v, a term t of type τ is interpreted as an element

[[t]] v ∈ [[v(τ )]]
and a formula f is interpreted as a Boolean value An interpretation is a pre-interpretation that is consistent with recursive and inductive denitions, that is:

[[f ]] v ,
For any recursive denition function f α (x) : τ = t and any s, we require

[[f s ]] to be such that, for all t, [[f s ]](t) = [[t]
] v where v maps the α to the s and the x to the t (and similarly for a predicate denition).

For any inductive denition p α (τ ) = f 1 | . . . |f l and any s, we require

[[p s ]]
to be the least predicate such that

[[f 1 ]] v , . . . , [[f l ]
] v hold where v maps the α to the s.

A set of closed formulas ∆ is satised by [[.]] if and only if [[f ]] v = for every
f ∈ ∆ and every valuation v. (Note that only the mapping of type variables in v is relevant here, since formulas are closed.) A set of closed formulas ∆ is satisable if and only if it is satised for some interpretation. Given a set of polymorphic closed axioms ∆ and a closed formula f to be proved, we may assume that f is monomorphic (otherwise we simply replace type variables in f by fresh type constants). Then we say that formula f is a logical consequence of ∆ if and only if the set ∆, not f is unsatisable.

[[n int ]]v = n [[r real ]]v = r [[xτ ]]v = v(xτ ) [[f τ1, . . . , τm (t1, . . . , tn)]]v = [[f v(τ1), . . . , v(τm) ]]([[t1]]v, . . . , [[tn]]v) [[let xτ = t1 in t2]]v = [[t2]] v[xτ →[[t 1 ]]v ] [[if f then t1 else t2]]v = [[t1]]v if [[f ]]v = , = [[t2]]v otherwise [[match t with p1 → t1 | . . . | pn → tn end]]v = [[ M (t, p1, t1, M (t, p2, t2, . . . , M (t, pn, tn, error )))]]v
Fig. 8. Interpretation of terms.

[[p τ1, . . . , τm (t1, . . . , tn Discussion. It is worth pointing out that our notion of interpretation does not prevent two distinct instances of a polymorphic symbol, say two types t s 1 and t s 2 or two functions f s 1 and f s 2 , to be interpreted in two completely dierent ways. Even for an algebraic data type, say list α , we do not require Nil s 1 and Nil s 2 to be identical. We simply require list s 1 to be the free algebra generated by Nil s 1 and Cons s 1 , and similarly list s 2 to be the free algebra generated by Nil s 2 and Cons s 2 . As a consequence, there is nothing wrong with an axiom dening a property of f int , for some polymorphic function f α , while all other instances are left uninterpreted. Even further, we could have two completely unrelated axioms for f int and f real , e.g. that f int is the identity over type int while f real is the square root function.

)]]v = [[p v(τ1), . . . , v(τm) ]]([[t1]]v, . . . , [[tn]]v) [[∀xτ . f ]]v = [[∃xτ . f ]]v = [[f1 • f2]]v = [[f1]]v • [[f2]]v where • ∈ {∧, ∨, ⇒, ⇔} [[not f ]]v = ¬[[f ]]v [[true]]v = [[false]]v = ⊥ [[let xτ = t1 in f2]]v = [[f2]] v[xτ →[[t 1 ]]v ] [[if f1 then f2 else f3]]v = [[f2]]v if [[f1]]v = , = [[f3]]v otherwise [[match t with p1 → f1 | . . . | pn → fn end]]v = [[ M (t,
M (t, xτ , b, h) = let xτ = t in b M (t, fi(), b, h) = if isfi(t) then b else h M (t, fi(p1, . . . , pn), b, h) = if isfi(t) then M (projf i,1 (t), p1, M (projf i,2 (t), p2, . . . , h), h) else h M (t, , b, h) = b M (t, p1 | p2, b, h) = M (t, p1, b, M (t, p2, b, h)) M (t, p as xτ , b, h) = let xτ = t in M (t, p, b, h)
Simply speaking, everything works as if we were using many-sorted logic with a possibly innite set of simple sorts (int, list int , list real , list list int , etc.), and a possibly innite set of functions and predicates with simple types (Nil int , Nil real , Cons list int , etc.), with suitable extensions for algebraic data types, recursive denitions, and inductive predicates.

Implementation

The logic we just described is implemented in Why3 at two dierent levels: an OCaml API and a surface language.

The OCaml API allows the user to build terms, patterns, formulas, declarations, and goals. The API is defensive: only well-typed values can be built, according to the typing rules of Sec. 2.2. Following the presentation above, one rst builds symbols and then, later, possible denitions for these symbols. This way, terms, patterns, and formulas can be built as soon as symbols are available, without the need of passing around a context containing denitions.

On top of this API, Why3 provides a surface language. Fig. 11 contains an example of input le. Contrary to the API, when a denition is provided, we do not separate the signature and the denition. For instance, we simply write type list 'a = Nil | Cons 'a (list 'a) to simultaneously introduce the type symbol list 'a, the two function symbols Nil and Cons (its constructors), and the algebraic data type denition.

In the surface language, there are no angle brackets . anymore. First, type variables are not explicitly bound in symbol declarations. They are rather gathered, as the set of all type variables appearing in the symbol's type. For instance, the declaration function length (l: list 'a) : nat = ... without having to pass int to Nil, Cons, and length. When the instantiation cannot be computed from the arguments, it must be provided. A typical example is the following: lemma L: length (Nil: list 'a) = O Without the type cast, this would result in an undefined type variable error. In both the API and the surface language, there is no type inference, only type checking. In particular, quantied variables are given types (such as forall m: nat in Fig. 11). This is a deliberate choice: we could implement type inference, but we think that specications are easier to read when types are given.

Among other features of the surface language of Why3 are type aliases (such as type t = list int) and tuple types. Type aliases are inlined systematically. Tuple types are particular cases of algebraic data types, and are generated on the y. There is also a syntax for record types (algebraic data types with a single constructor and named projection functions). Finally, logic declarations are organized in units called theories, as shown in Fig. 11. Theories can refer to and instantiate other theories. We do not discuss theories here; see [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF] for details.

Targeting Multiple Provers

We now explain how Why3 translates the logic we just described into the native input format of external theorem provers. Currently, Why3 supports the following theorem provers: Proof assistants: Coq 8.4 [41] and PVS 6.0 [START_REF] Owre | PVS: A prototype verication system[END_REF]; SMT solvers: Alt-Ergo 0.95.1 [START_REF] Bobot | The Alt-Ergo automated theorem prover[END_REF], CVC3 2.4.1 [START_REF] Barrett | CVC3[END_REF], CVC4 1.0 [START_REF] Barrett | CVC4[END_REF], Simplify 1.5.4 [START_REF] Detlefs | Simplify: a theorem prover for program checking[END_REF], Yices 1.0.38 [START_REF] De Moura | Yices: An SMT Solver[END_REF] and Yices2 2.0.4, Z3 4.3.1 [START_REF] De Moura | Z3, an ecient SMT solver[END_REF]; ATP systems: E 1.6 [START_REF] Schulz | System description: E 0.81[END_REF], iProver 0.8.1 [START_REF] Korovin | iProver an instantiation-based theorem prover for rst-order logic (system description)[END_REF], SPASS 3.7 [START_REF] Weidenbach | SPASS version 3.5[END_REF], Vampire 0.6 [START_REF] Riazanov | Vampire[END_REF], Zenon 0.7.1 [START_REF] Bonichon | Zenon : An extensible automated theorem prover producing checkable proofs[END_REF]; Dedicated provers: Gappa 0.15.1 [START_REF] Daumas | Certication of bounds on expressions involving rounded operators[END_REF], Mathematica 8.0.

We only list the most recent versions that are supported; some older versions may be supported as well.

Tasks and Transformations

A central notion in Why3 is that of task. A task is a context Γ (symbols, possibly with denitions), a set of axioms ∆, and a formula to be proved. Tasks are massaged using transformations until they reach a subset of Why3's logic that coincides with the input format of a theorem prover. A transformation turns a task into a set of new tasks. Key transformations are the following: elimination of recursion, inductive predicates, algebraic data types and pattern matching, if-then-else construct, let binding; encoding of types, to target many-sorted or untyped logic [START_REF] Couchot | Handling polymorphism in automated deduction[END_REF][START_REF] Bobot | Expressing Polymorphic Types in a Many-Sorted Language[END_REF].

In the process of proving a task, other transformations may be used, such as inlining, splitting, various kinds of simplication, or even induction (following Leino [START_REF] Leino | Automating induction with an SMT solver[END_REF]). Why3 can be extended with new transformations via OCaml plugins. The OCaml API allows the user to build tasks and to apply transformations eciently (thanks to memoization).

Drivers

The way a particular prover is handled in Why3 is controlled by a text le called a driver. Such a le lists the transformations that must be applied to a task prior to its transmission to the prover, denes the pretty-printer that must be used when we are done with transformations, lists symbols and axioms that are built-in in the prover, and provides regular expressions to interpret the output of calls to the prover.

For instance, the driver for SPASS refers to the printer registered under the name tptp-fof, includes transformations such as eliminate algebraic (to get rid of algebraic data types and pattern matching) and encoding tptp (to encode types), and states that equality is built-in with syntax (x=y), among other things.

Users may dene new drivers, to add support for a new prover or to experiment with alternative ways of using a prover (e.g. not making use of a built-in theory, or using an alternate input format). For that purpose, Why3 can be extended with new pretty-printers via OCaml plug-ins. The OCaml API provides ways to load a driver and then to use it to call the corresponding theorem prover on a task. Drivers are described in more details in our earlier work [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF].

Prover Specicities. There are several places where we have to be careful to avoid introducing inconsistencies in the process of translating from Why3 to theorem provers.

An example is integer division. Why3 standard library contains two theories: one for Euclidean division, and another where division rounds towards zero as in most programming languages. When it comes to using a built-in notion of division provided by some prover, we have to identify which one it is, if any, or to provide workarounds otherwise, if possible. For instance, Z3 provides Euclidean division and modulo, but CVC4 provides a division that appears to be none of the two divisions from Why3 standard library.

Another example is the fact that all types in Why3 are inhabited. Automated theorem provers typically make that assumption already. When it comes to proof assistants Coq and PVS, however, it is not granted for free. PVS provides a builtin mechanism for non-empty types, that we use readily. Coq, on the contrary, does not provide any such facility. We resort to type classes to ensure that all types we manipulate are inhabited. For instance, function length is translated into Fixpoint length {a:Type} {a_WT:WhyType a} (l:(list a)) ... where WhyType a is a type class that states that type a is inhabited and has decidable equality.

Proof Sessions

When a verication tool is built on top of a single automated prover, it is straightforward to replay a proof: one simply reruns the tool on the input les. The same applies for a proof that has been built interactively, say with Coq or KIV, and stored into les: it can be rechecked easily, in batch mode.

With Why3, the situation is somewhat dierent. Using the graphical user interface why3ide, the user interactively applies transformations and calls external theorem provers, until all goals are discharged. Calls to provers record the maximal amount of CPU time and memory that is allocated to the prover. Calls to proof assistants record user-edited proof scripts. All that information is stored into a set of les called a proof session. This way, it can be reloaded on a subsequent call to why3ide or replayed in a batch mode with another tool, why3replayer. This is of particular interest when the user upgrades the version of one or several provers. A run of why3replayer then tells whether the proof session is still valid or must be updated. Proof sessions are the subject of another publication [START_REF] Bobot | Preserving user proofs across specication changes[END_REF].

Examples

We now give some examples of the way goals are translated to be passed to theorem provers. Let us consider our running example in Fig. 11 and let us assume that we are targeting the SMT solver Alt-Ergo. Algebraic Data Types. We must get rid of algebraic data types. Thus, list 'a is simply turned into some uninterpreted data type, together with uninterpreted function symbols for constructors type 'a list logic Nil : 'a list logic Cons : 'a, 'a list → 'a list and axioms (not shown here) to state that Nil and Cons are distinct and that Cons is injective. To get rid of pattern matching on type list, we also introduce a function symbol logic match_list : 'a list, 'a1, 'a1 → 'a1 together with axioms stating that match list(Nil, a, b) = a and that match list(Cons(x, y), a, b) = b. We proceed similarly for type nat.

Recursive Denitions. We must also get rid of the recursive denition of function fof(length_nil, axiom, ![A]: sort(int, length(sort(list(A),nil))) = sort(int,const_0)).

fof(g, conjecture, sort(int, length(sort(list(int), nil))) = sort(int,const_0)).

Here sort is a binary function symbol that wraps terms with types. Types themselves are represented as regular terms, such as constant int or variable A above. The case of an SMT solver is more subtle, as we need to protect built-in types such as integers, arrays, or reals if we want to use built-in decision procedures [START_REF] Bobot | Expressing Polymorphic Types in a Many-Sorted Language[END_REF].

Experimental Results

In this section, we use Why3 to run a small benchmark of 8 dierent automated provers. The experiment uses 83 proof sessions from our gallery, corresponding to logical theories or programs that were all successfully proved. This includes our solutions to several recent competitions in program verication (VSTTE 2012, FoVeOOS 2011, VSTTE 2012, FM 2012). The total number of subgoals is 2849.

For each subgoal that was discharged by at least one prover, we run the other 7 provers on that subgoal, with the same limit of CPU time that was given to the rst one. Provers are run on an 8-cores 3.20GHz Intel Xeon with 24Gb of RAM. Each prover runs on a separate core, with a limit of 1Gb of memory. Results are given in Table 1. For each prover, we give the total number of goals proved, and the maximum/average running time per goal.

The purpose of that table is not really to compare provers, but rather to show the benets of a collaborative use of several provers: if we were using CVC3 only, we would be left with 646 (= 2849 -2203) unproved subgoals. Besides, it is worth pointing out that most of these goals involve arithmetic; yet provers with no support for arithmetic (E, SPASS, and Vampire, in that case) are able to discharge a large subset of the goals. This was rather unexpected and encourages us to increase our daily use of these provers and to improve the way we use them even further. [START_REF] Blanchette | Encoding monomorphic and polymorphic types[END_REF] Related Work

There is actually very little in the literature regarding the extension of rstorder logic with polymorphism. For instance, a classical textbook such as Manzano's [START_REF] Manzano | Extensions of rst order logic[END_REF] does not contain a single occurrence of the word `polymorphism'.

One the other side of the logical spectrum, rich logics such as the Calculus of Inductive Constructions or HOL do have polymorphism (even beyond rank-1) but are seldom interested in identifying their rst-order fragments. Among the recent work on this subject, we can mention the work by Leino and Rümmer on Boogie 2's type system [START_REF] Leino | A polymorphic intermediate verication language: Design and logical encoding[END_REF] and the denition of the TPTP TFF1 format by Blanchette and Paskevich [START_REF] Blanchette | TFF1: The TPTP typed rst-order form with rank-1 polymorphism[END_REF].

There is more related work regarding the second part of this paper, as a lot has been done in the context of Isabelle's Sledgehammer tactic [START_REF] Meng | Translating higher-order clauses to rst-order clauses[END_REF][START_REF] Böhme | Sledgehammer: Judgement day[END_REF]. It translates Isabelle's logic to several external provers, using type encodings dierent from ours, ranging from mere type erasure (which is unsound, but Sledgehammer uses proof reconstruction5 ) to partial monomorphisation [START_REF] Blanchette | Encoding monomorphic and polymorphic types[END_REF] (which is proved incomplete [START_REF] Bobot | Expressing Polymorphic Types in a Many-Sorted Language[END_REF] but seems ecient in practice anyway). Earlier, Hurd had already investigated encodings from higher-order to rst-order logic [START_REF] Hurd | An lcf-style interface between hol and rst-order logic[END_REF].

Conclusion and Perspectives

We have presented a logic whose purpose is to provide a unied front-end to many existing theorem provers, either interactive or automated, and its implementation in Why3. We have designed this logic with the idea that specication must be as natural as possible and that tools should adapt themselves to proof obligations (and not the opposite). Using a wide range of theorem provers encourages this attitude. One of the key features of our logic is polymorphism. It is dened and handled roughly the same way it is in tools Boogie, Sledgehammer, and Alt-Ergo. There

  . . , α (τ, . . . , τ ) : τ function symbol declaration d p ::= p α, . . . , α (τ, . . . , τ ) predicate symbol declaration

Fig. 7 .

 7 Fig. 7. Typing rules for patterns.

  according to the denitions given in Fig.89. Note that pattern matching is compiled away as show in Fig.10. Operator M turns a match construct into elementary tests. More precisely, M (t, p, b, h) lters value t against pattern p and returns b in case of success and h in case of failure. Since type checking ensures that any pattern matching is exhaustive, the error term cannot actually appear in the result of M . It is only used to simplify the denition and use of function M .

Fig. 9 .

 9 Fig. 9. Interpretation of formulas.

Fig. 10 .

 10 Fig. 10. Interpretation of patterns.

Fig. 11 .

 11 Fig. 11. Example of Why3 input le.

  length. It is turned into some uninterpreted function symbol together with two axioms: logic length : 'a list → nat axiom length_def : length(Nil : 'a list) = O axiom length_def1 : forall x:'a. forall x1:'a list. length(Cons(x, x1)) = S(length(x1)) Note that we are not making use of function match_list here, since it immediately reduces to simpler axioms. Inductive Denitions. Finally, we must get rid of the inductive denition of predicate even. It is axiomatized as follows: logic even : nat → prop axiom EvenO : even(O) axiom EvenS : forall m:nat. even(m) → even(S(S(m))) axiom even_inversion : forall z:nat. even(z) → (z = O or exists m:nat. even(m) and z = S(S(m)))

  a with . . . with a algebraic data types | recursive δ with . . . with δ recursive denitions | inductive i with . . . with i inductive predicates a ::= d t = d f | . . . |d f

		algebraic data type
	δ ::= function f α, . . . , α (x τ , . . . , x τ ) : τ = t function denition
	| predicate p α, . . . , α (x τ , . . . , x τ ) = f predicate denition
	i ::= d p = f | . . . |f	inductive predicate

  nat) : nat, Nil α : list α , Cons α (α, list α ) : list α , length α (list α ) : nat,

	t ::= c int	literal integer constant
	| c real	literal real constant
	| xτ	variable
	| f τ, . . . , τ (t, . . . , t)	function symbol application
	| let xτ = t in t	local binding
	| if f then t else t	conditional expression
	| match t with p → t | . . . | p → t end pattern matching
	Fig. 1. Syntax for terms.
	f ::= p τ, . . . , τ (t, . . . , t)	predicate symbol application
	| ∀xτ . f	universal quantication
	| ∃xτ . f	existential quantication
	Pair α 1 , α 2 (α 1 , α 2 ) : pair α 1 , α 2 }
	Σ P = {= α (α, α), even(nat)}

  Let Γ be the extension of the signature above with the following set of denitions:datatype nat = O | S(nat) datatype list α = Nil α | Cons α (α, list α ) recursive function length α (l list α ) : nat = match l list α with Nil α → O | Cons α ( , r list α ) → S(length(r list α )) end inductive even(nat) =even(O) | ∀n nat . even(n nat ) ⇒ even(S(S(n nat )))

		end pattern matching
	Fig. 2. Syntax for formulas.
	p ::= xτ	variable
	| f τ, . . . , τ (p, . . . , p) constructor application
	|	catch all
	| p | p	or pattern
	| p as xτ	binding
	Fig. 3. Syntax for patterns.

Table 1 .

 1 This is incomplete, since we cannot capture the minimality of even in rst-order logic. For instance, Alt-Ergo cannot prove the goal forall x: nat. even x → not (even (S x)), while we could use Coq to prove it. Anyway, Alt-Ergo easily manages to prove the goal Comparing eight automated provers using Why3.Types. As we see on the example above, we did not have to encode types. Indeed, Alt-Ergo supports polymorphic types[START_REF] Bobot | Implementing Polymorphism in SMT solvers[END_REF]. If we are instead targeting a prover that only supports simple types (e.g. Z3) or some untyped logic (e.g. SPASS), we have to encode the polymorphic types of Why3 in some way or another. For instance, on the following Why3 input

	goal G: even(length(Cons(O, Cons(O, (Nil : nat list)))))
	with suitable instantiations of lemmas length_def, length_def1, EvenO, and
	EvenS.

the le that is passed to SPASS is the following:

We use automated provers to denote both SMT solvers and ATP systems.

A signicant dierence between Sledgehammer and our work is that we do not perform any kind of proof reconstruction. Thus we have to keep to sound encodings.

Acknowledgments. I would like to thank Andrei Paskevich and Sylvain Conchon for fruitful discussions during the preparation of this paper. Some ideas behind the formalization in Sec. 2 already appear in Bobot and Paskevich's work [11]. The development of Why3 is joint work with François Bobot, Claude Marché, Guillaume Melquiond, and Andrei Paskevich.

is no competition, but rather a nice convergence. A contribution of this paper is to add the formalization of algebraic data types, recursive denitions, and inductive predicates on top of that.

Currently, Why3 is successfully used as a sub-component in various projects [START_REF]The Frama-C platform for static analysis of C programs[END_REF][START_REF] Marché | The Krakatoa tool for certication of Java/JavaCard programs annotated in JML[END_REF][START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF][START_REF] Comar | Integrating formal program verication with testing[END_REF], as well as the vehicle for many non-trivial case studies in program verication (see for instance [START_REF] Filliâtre | Verifying two lines of C with Why3: an exercise in program verication[END_REF]). We also envision that verication environments that are currently built on top of a dedicated prover (e.g. B, KIV, SmallFoot) could also benet from additional, external theorem provers. For instance, we are currently experimenting with the use of Why3 to discharge goals obtained from Atelier B [START_REF] Mentré | Discharging proof obligations from Atelier B using multiple automated provers[END_REF], and the rst results are promising.

We could still improve the way we are using theorem provers. For instance, we can observe that some tools that are based on a single automated prover e.g. VCC, Dafny, or VeriFast are able to carry out impressive case studies. It is clear that these tools are achieving a level of intimacy with the prover that is beyond that of Why3. We should learn from these tools and transpose relevant techniques to Why3. In particular, we our support of built-in theories.

Of course, it would be much simpler if we had native support for polymorphic types in provers. Alt-Ergo demonstrates that this is possible, and even simple to implement [START_REF] Bobot | Implementing Polymorphism in SMT solvers[END_REF], yet this is currently the only automated prover with such a feature. We hope that TFF1 [START_REF] Blanchette | TFF1: The TPTP typed rst-order form with rank-1 polymorphism[END_REF] will encourage some ATP developers to take the plunge.