Christine Paulin-Mohring
email: christine.paulin@lri.fr

Introduction to the Calculus of Inductive Constructions

Introduction

The Calculus of Inductive Constructions (CIC) is the formalism behind the interactive proof assistant Coq [START_REF] Coq | The Coq Proof Assistant Reference Manual -Version V8.4[END_REF][START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF]. It is a powerful language which aims at representing both functional programs in the style of the ML language and proofs in higher-order logic. Many data-structures can be represented in this language: usual data-types like lists and binary trees (possibly polymorphic) but also infinitely branching trees. At the logical level, inductive definitions give a natural representation of notions like reachability and operational semantics defined using inference rules.

Inductive definitions in the context of a proof language were formalised in the early 90's in two different settings. The first one is Martin-Löf's Type Theory [START_REF] Martin-Löf | Intuitionistic Type Theory[END_REF]. This theory was originally presented with a set of rules defining basic notions like products, sums, natural numbers, equality. All of them (except for functions) are an instance of a general scheme of inductive definitions which has been studied by P. Dybjer [START_REF] Dybjer | Inductive families[END_REF]. The second one is the pure Calculus of Constructions. This is a typed polymorphic functional language, which is powerful enough to encode inductive definitions [START_REF] Böhm | Automatic synthesis of typed λ-programs on term algebras[END_REF][START_REF] Pfenning | Inductively defined types in the Calculus of Constructions[END_REF], but this encoding has some drawbacks: efficiency of computation of functions over these data-types and some natural properties that cannot be proven. The extension of the formalism with primitive inductive definitions [START_REF] Th | Inductively defined types[END_REF][START_REF] Paulin-Mohring | Inductive Definitions in the System Coq -Rules and Properties[END_REF] was consequently a natural choice. In proof assistants based on higher-order logic (HOL), an impredicative encoding of inductive definitions is used: this is made possible by the existence of a primitive infinite type (including integers) and the fact that HOL is only concerned by extensional properties of objects (not computations) [START_REF] Paulson | A fixedpoint approach to implementing (co)inductive definitions[END_REF].

Inductive definitions, as a primitive or derived notion are one of the main ingredients of the languages for interactive theorem proving both for representing objects and logical notions.

In this paper, we give a quick overview of the Calculus of Inductive Constructions, the formalism behind the Coq proof assistant. In section 2, we present the language and the typing rules. We start with the pure functional part and then continue with the inductive declarations. We shall then briefly discuss the properties of this language in section 3, both from the theoretical and pragmatic points of view. We shall then conclude with examples of applications, the description of some of the trends in sections 4,5 and 6.

Proof System

The Calculus of Constructions

The Calculus of Constructions which is the purely functional language underlying the Calculus of Inductive Constructions has been introduced by Coquand and Huet [START_REF] Th | Constructions: A higher order proof system for mechanizing mathematics[END_REF][START_REF] Th | The Calculus of Constructions[END_REF]. It can be defined as a pure type system (PTS). A PTS is a typed lambda-calculus with a unique syntactic language describing both terms and types. Terms include variables, (typed) abstractions (written fun x : A ⇒ t) and applications (written t u) as in ordinary lambda-calculus. The type of an abstraction is a (dependent) product Πx : A, B making possible for the type B of t to depend on the variable x. The notation A → B for the type of functions from type A to type B is just an abbreviation in the special case where B does not depend on x. Types are themselves typed objects, the type of a type will be a special constant called a sort. There is at least one sort called Type. Different PTS depend on the set of sorts we start with (each sort corresponds to a certain universe of objects) and also which products can be done (in which universes).

For instance, with A a type, the identity function fun x : A ⇒ x is a term of type A → A. With A being a type variable, we may build the polymorphic identity fun A : Type ⇒ fun x : A ⇒ x of type ΠA : Type, A → A.

In the case of the Calculus of Constructions, we have an infinite set of sorts S def = {Prop} ∪ i∈N {Type i }. The sort Prop captures the type of expressions which denote logical propositions. We follow the Curry-Howard correspondence where a proposition A is represented by a type (namely the type of proofs of A) and a proof of the logical proposition A will correspond to an object t of type A. If A and B are two types corresponding to logical propositions, then the proposition A ⇒ B will be represented by the type A → B of functions transforming proofs of A into proofs of B, the proposition A ∧ B will be represented by the type A × B of pairs build with a proof of A and a proof of B. Given a type T , the type Πx : T, B will represent the type of dependent functions which given a term t : T computes a term of type B[t/x] corresponding to proofs of the logical proposition ∀x : T, B. Because types represent logical propositions, the language will contain empty types corresponding to unprovable propositions.

Notations. We shall freely use the notation ∀x : A, B instead of Πx : A, B when B represents a proposition. We write t[u/x] for the term t in which the variable x has been replaced by the term u. The term t u 1 . . . u n represents (. . . (t u 1 ) . . . u n ) and fun (x

1 : A 1 ) . . . (x n : A n ) ⇒ t (resp. Π(x 1 : A 1 ) . . . (x n : A n ), B) is the same as fun x 1 : A 1 ⇒ . . . fun x n : A n ⇒ t (resp. Πx 1 : A 1 , . . . Πx n : A n , B). The term A → B → C should be understood as A → (B → C) and Πx : A, B → C is the same as Πx : A, (B → C).
We sometimes omit the type of the variable in abstractions and products when they are clear from the context.

In higher-order logic, propositions and objects are written using the same functional language with abstractions and applications. We may want to introduce a binary relation on a type A as a variable R. This variable will have type A → A → Prop (this type replaces an arity declaration in first-order logic). We can build a predicate fun x : A ⇒ R x x representing the set of objects which are in relation with themselves, this predicate will have type A → Prop (this expression shall not be confused with the type ∀x : A, R x x of type Prop, expressing the reflexivity of R).

We need A → A → Prop to be a well-formed type, which means it is typed with a sort. This sort will be Type 1 . If we want to iterate constructions on Type 1 , we shall need this sort itself to be well-typed, that will require introducing a new sort Type 2 to be the type of the object Type 1 . The need for an infinite hierarchy of universes comes from the fact that the more naive system where we have only one sort Type of type Type is inconsistent.

The Calculus of Inductive Constructions manipulates judgements which are of the form

x 1 : A 1 , . . . , x n : A n ⊢ t : A
In this judgement, x 1 : A 1 , . . . , x n : A n is called the context and the part t : A on the righthand side of the ⊢ sign is called the conclusion. In the context, x i is a variable declared of type A i representing the name of an object. Following the propositions as types paradigm, when A i denotes a logical proposition, x i will be a name given to the hypothesis that A i holds. The judgement can be read as: under the assumption that we have objects x i of type A i , the term t is well-formed of type A.

For instance, in order to reason on Peano integers, it is possible to introduce a signature with a type variable N : Type for representing the type of Peano integers, an object z : N (for zero) and an object S : N → N for the successor function. We call Γ S the context N : Type, z : N, S : N → N . The following judgements are derivable :

Γ S ⊢ z : N Γ S ⊢ S z : N Γ S ⊢ S (S z) : N
It is also possible to introduce a binary relations le which represents the natural order on N . We shall add le : N → N → Prop and hypotheses like lez : ∀x : N, le z n and leS : ∀x y : N, le x y → le (S x) (S y). We introduce a new context

Γ N def = Γ S , le : N → N → Prop, lez : (∀x : N, le z x), leS : (∀x y : N, le x y → le (S x) (S y))
We shall be able to derive

Γ N ⊢ lez z : le z z Γ N ⊢ leS z z (lez z) : le (S z) (S z)
It is easy, for every natural number n to find a term l n such that Γ N ⊢ l n : le (S n z) (S n z). We can do it (at the meta level) via a simple induction on n. It would be nice to prove internally the property ∀x : N, le x x but our context is too weak for that because it contains no induction property, so N might contain more objects than the ones written S n z. In first-order logic, the induction principle for a property P is added for every possible property P , leading to an infinite set of axioms. In a higher-order logic like the Calculus of Constructions it is sufficient to add a single proposition as an axiom that will contain a quantification over all possible properties P . We introduce Γ P def = Γ N , ind : (∀P : N → Prop, P z → (∀x : N, P x → P (S x)) → ∀x : N, P x) and we can derive the judgement

Γ P ⊢ ind (fun x : N ⇒ le x x)(lez z)(fun (x : N )(I : le x x) ⇒ leS x x I) : ∀x : N, le x x
Type-checking proof-terms can be tricky and cumbersome. The user usually does not want and does not need to do it, because proofs are built just interacting with the properties that have to be proven using high-level programs called tactics (see section 3.2). However, the proof-term is always build underneath by the system and given for type checking (which is also proof-checking) to a trusted kernel of the system that will guaranty the absence of flaw in the proof. This proof term can be checked independently by different programs and the information contained in the proof term can also be used for instance for analysing dependency and intelligent printing. We comment some rules in figure 1. There are two different rules for typing a product Πx : A, B. In both cases the term B should be well-typed in a context where we have x : A and its type should be a sort s. When s is Prop, then the product stays in Prop even if A itself lies in a bigger universe. So ΠX : Prop, X → X has type Prop. We say that Prop is an impredicative sort, because one can build new objects in Prop using a universal quantification on the class of all objects in Prop (including the one currently defined). Impredicative systems are powerful but also very fragile in the sense that impredicativity does not interact very well with other features leading rapidly to inconsistent systems. For instance we have Prop of type Type 1 but Prop only can be impredicative, the impredicativity of Type 1 gives an inconsistent system [START_REF] Th | An analysis of girard's paradox[END_REF], so if we want to build the type ΠX : Type 1 , X → X we need a bigger universe Type 2 .

Γ ⊢ t : A Γ ⊢ B : s A B Γ ⊢ t : B
Another interesting rule is the last one, called the conversion rule. It says that a term of type A can be also seen as a term of type B, given B is well-formed and the relation A B holds. This relation serves two purposes. First it implements the universe cumulativity, Prop Type 1 and Type i Type i+1 : any term typed in one universe can be considered as an element of a bigger universe. Second, it implements the fact that types are considered modulo computation (namely βequivalence in the current system). The β-reduction rule implements function computation namely the fact that an abstraction of a term t over a variable x applied to a term a behaves like the term t in which x has been replaced by a: (fun x : A ⇒ t) a ≃ t[a/x]. An important aspect of this rule is that this is the same term which is typed by A and by B, so these computation steps are done automatically and do not leave traces in the proof-term. We shall come back to this feature in section 3.2.

Using this purely functional part, it is possible to encode many interesting notions. For instance ∀C : Prop, C is a logical proposition (a term of type Prop) which encodes absurdity (⊥) : there is no closed term of type ∀C : Prop, C (so no proof of ⊥ without hypothesis) and also from a proof t of ∀C : Prop, C one can build a proof t C of an arbitrary proposition C so the natural deduction rule for eliminating ⊥ is derivable in the logic.

It is also possible to encode an existential quantification (using a universal quantification in a negative position)

Γ ⊢ t = t Γ ⊢ t = u Γ, x : A ⊢ B : Prop Γ ⊢ B[t/x] Γ ⊢ B[u/x]

Inductive Definitions

Inductive definitions are introduced on top of the pure Calculus of Constructions. Their main purpose is to provide an efficient representation of data-types.

A new inductive definition can be added to the environment: it requires to specify its name, its arity (the type of the inductive definition) and the set of its constructors.

Examples For instance, natural numbers defined with two constructors z and S, can be introduced as before with the following declaration:

Inductive N : Type := z : N | S : N → N.
This declaration adds new typed objects N : Type, z : N, S : N → N in the context. But unlike in the first-order case, the logic captures the fact that N is the initial algebra relatively to these two operations, consequently we shall be able to build functions of type N → A using the initially property and to derive properties like ∀x : N, S x = z and ∀x y : N, S x = S y → x = y. Also the induction principle is provable.

Inductive definitions are also used for defining relations. The order on natural numbers can be defined using the properties we gave as axioms before:

Inductive le : N → N → Prop := lez:∀x, le z x | leS:∀x y, le x y → le (S x) (S y).

This declaration introduces le : N → N → Prop, lez : (∀x : N, le z x), leS : (∀x y : N, le x y → le (S x) (S y)) in the context, we shall also be able to prove the fact that le is the smallest relation R such that ∀x : N, R z x and ∀x y : N, R x y → R (S x) (S y). It gives us a powerful way to prove lemmas of the form ∀x y : N, le x y → R x y.

Inductive definitions can be defined with parameters. For instance the reflexive-transitive closure of a binary relation R on a type A can be defined as an inductive definition RT with A and R as parameters:

Inductive RT A (R : A → A → Prop) : A → A → Prop := RTrefl:∀ x, RT A R x x | RTR:∀ x y, R x y → RT A R x y | RTtran:∀ x y z, RT A R x z → RT A R z y → RT A R x y.
We have three constructors for this definition: RTrefl states that the reflexive-transitive closure is reflexive, RTR says it contains R and RTtran that it is transitive. For instance, we can prove that the reflexive-transitive closure of the successor relation on N is equivalent to the previously defined le relation: ∀ x y, le x y ↔ RT N (fun x y ⇒y=S x)

Inductive definitions are also used to encode logical operations like absurdity (a definition with no constructor) existential quantification or equality.

Inductive False : Prop := . Inductive ex A (P:A→Prop) : Prop := exists : ∀ x, P x → ex A P. Inductive eq A (x:A) : A → Prop := eqrefl : eq x x.

In first-order logic, when axioms are introduced to form a theory, there is always a risk that it has no model, and consequently everything can be proven. This cannot happen with inductive definitions: there are syntactic restrictions on the type of constructors that ensures the existence of a model.

General rules. The general pattern for declaring an inductive definition is

Inductive I pars : Ar := ... | c : Π(x 1 : A 1 )..(x n : A n ), I pars u 1 ..u p | ...

Coq allows the declaration of mutually inductive definitions but, for the sake of simplicity, we shall not give the details here. We introduce some terminology -pars are called the parameters of the inductive definition and will be the same for all definitions; -Ar is called the arity; -u i is an index ; -Π(x 1 : A 1 )..(x n : A n ), I pars u 1 ..u p is a type of constructor -A i is a type of argument of constructor There are conditions to accept that the definition is well-formed:

-An arity has the form Π(y 1 : B 1 )..(y p : B p ), s, with s a sort which is called the sort of the inductive definition. -Type of constructors C are well-typed:

(I : Πpars, Ar), pars ⊢ C : s

• if s is predicative (not Prop) then the condition above on C requires the type of arguments of constructors to be in the same universe: for all i, A i : s or A i : Prop • if s is Prop, we distinguish between predicative definitions where A i : Prop for all i and impredicative definitions otherwise, meaning there is at least one i such that A i has type Type i and not Prop.

There is also a positivity condition: occurrences of I should only occur strictly positively in types of arguments of constructors A i which means that we are in one of these cases:

non-recursive case: I does not occur in A i simple case: A i = I t 1 . . . t p (not necessarily the same parameters), I ∈ t k functional case: A i = Πz : B 1 , B 2 with I ∈ B 1 and I strictly positive in B 2 -nested case: A i = J t 1 . . . t q with J another inductive definition with parameters X 1 . . . X r . When t 1 . . . t r are substituted for X 1 . . . X r in the types of constructors of J, the strict positivity condition should still be satisfied. We also need I ∈ t k for r < k ≤ q.

The language of the PTS is extended with access to the inductive definition and its constructors plus two new constructions for pattern-matching and fixpoint.

The inductive definition itself is a new constant, its type is given by its arity and is generalised with respect to the parameters.

I : Πpars, Ar

The Calculus of Constructions follows the logical rules of natural deduction where each concept is associated with introduction and elimination rules. A computation rules explains how a combination of introduction and elimination rules for the same notion (a cut) can be eliminated.

In the case of inductive definitions, introduction rules are given by the constructors. Given that c is the i-th constructor of an inductive definition I with parameters pars and type of constructor C, we have:

c ≡ Constr(i, I) : Πpars, C
Elimination rules use two different notions: a pattern-matching rule extended for dependent types (each branch can have a different type, depending on the constructor) and a (restricted) fixpoint construction for recursive definitions.

The primitive rule for pattern-matching comes in a very primitive way: it covers one level of constructors and should be complete (one branch for each constructor):

t : I pars t 1 . . . t p y 1 . . . y p , x : I pars y 1 . . . y p ⊢ P : s ′ {x 1 : A 1 . . . x n : A n ⊢ f : P [u 1 /y 1 , . . . , u p /y p , (c x 1 . . . x n )/x]} c match t as x in I y 1 . . . y p return P with . . . | c x 1 . . . x n ⇒ f | . . . end : P [t 1 /y 1 , . . . , t p /y p , t/x]
Reduction rule. The reduction rule (called ι) applies when t starts with a constructor and is as expected (reduces to the corresponding branch after instantiating the pattern variables with the arguments of the constructor).

Examples. This unique rule covers many different situations. In Coq high-level language that we shall use in the examples, we can generally omit the information as x, in I y 1 . . . y p and return P .

The match construction can be used to define a function by pattern-matching like the predecessor function.

Definition pred (x:N) : N := match x with z ⇒ z | S n ⇒ n end.

in this case the return predicate is just P def = N. The same match rule can be used to reason by case analysis on integer and prove the following principle: ∀P : N → Prop, P z → (∀x, P (S x)) → (∀x, P x) Given P , Hz : P z and HS : ∀x, P (S x) the following case has type ∀x, P x Definition case (x:N) : P x := match x with z ⇒ Hz | S n ⇒ HS n end.

In this example the return predicate is just P n and the two branches have two different types: P z for the first one and P (S n) for the second.

The two previous constructions are available in most formalisms. One specificity of CIC is to allow also the definition of new types by pattern-matching. An example can be found when we want to study the semantic of a program and model an environment mapping variables to values. We can represent variables by natural numbers and an environment by a function of type N → T . However with this simple function type, all values should be in the same type. Assume we know a more precise type for some of the variables (the variable 0 as type N and the variable 1 is N → N , other variables are in a default type T ), we may want to capture this in the type of environments. We can do it with a construction similar to pred but returning a Type as the result instead of a number:

Definition env (x:N) : Type := match x with z ⇒ N | S z ⇒ N → N | S (S x) ⇒ T end.

In this example we use a more elaborate pattern-matching construction that Coq compiles into the primitive forms (using two nested simple pattern-matching). The reduction rule gives us the following equivalence between expressions:

env z ≃ N env (S z) ≃ N → N env (S (S x)) ≃ T
We need again to use the match construction to build a specific environment, but now each branch as a different type, the return predicate is env x.

Definition e1 (x:N) : env x := match x with z ⇒ S (S z) | S z ⇒ (fun x : N ⇒ z) | S (S x) ⇒ t end.

The result S (S z) in the first branch (constructor z) has type N which is equivalent to the expected type env z. The result (fun x : N ⇒ z) in the second branch (constructor S z) has type N → N which is equivalent to the expected type env (S z), the last branch returns a default value t in type T which is equivalent to the expected type env (S (S x)).

The match operation is also available for inductive relations. For instance, for the equality, it gives us the elimination principle we mentioned before

Γ ⊢ e : t = u Γ, x : A ⊢ B : Prop Γ ⊢ f : B[t/x] Γ ⊢ match e in = x return B with eqrefl ⇒ f end : B[u/x]
Actually the match rule gives us a stronger rule, called a dependent elimination, which allows to replace (in certain contexts) a proof e of t = u by eqrefl t.

If we take the definition of le, the match operation will be useful to prove a property like le (S x) z → ⊥. Intuitively this is because no constructor can give a proof of an instance of le (S x) z. Building the proof term requires to define an invariant relation inv x y that will be true for all x, y such that le x y but will be false for (S x) z. It is easily done using match to define a proposition which is ⊥ for (S x) z and ⊤ for all the other values. We use Coq high-level syntax. Type-checking conditions. The main restriction lies in the relation between the sort s of the inductive definition and the sort s ′ of the pattern-matching. When s is Type, which means that we have a predicative inductive definition, then we can have any possible sorts s ′ for case analysis.

When s is Prop however, the question is a bit more tricky for several reasons:

-Prop is an impredicative sort, so uncareful elimination can easily introduce paradoxes; -it is sometimes useful to add an axiom of proof irrelevance for propositions (which says that two different proofs of the same property can be considered as equal) so while it is good to be able to prove that for instance true = false, a similar mechanism that will lead to two terms (representing proofs of) in A ∨ B that are provably different is less desirable; -Prop is used for program extraction: any term in A : Prop is removed during extraction so should not be needed for computing the informative art, in a pattern-matching is done on a term in an inductive definition in Prop, but with the result being used for computing, then we need to be able to execute the match without executing the head, which is only feasible in specific cases.

For an inductive definition of sort Prop, the only elimination allowed is on the sort Prop itself. There are exceptions where any elimination is allowed: in the specific case where I is a predicative definition with only zero or one constructor with all its arguments A i : Prop. The exception covers cases like absurdity, equality, conjunction of two propositions, accessibility. . . In general, an expression fix f (x 1 : A 1 ) . . . (x n : A n ) : B := t is well typed of type B when t is well-typed of type B in an environment containing (f : Π(x 1 : A 1 ) . . . (x n : A n ), B) and (x 1 : A 1 ) . . . (x n : A n ); -t satisfies an extra syntactic condition that recursive calls to (f u 1 . . . u n ) in t are made on terms u n structurally smaller than x n .

The reduction rule is the usual fixpoint reduction except that in order to avoid infinite loops, it is only activated when the n-th argument of the fixpoint starts with a constructor.

The current inductive definitions of Coq present certain drawbacks. The syntactic condition for accepting fixpoints is very sensitive and not well-suited when developing a proof using tactics. Different approaches using type annotations have been proposed instead (for instance [START_REF] Abel | A Polymorphic Lambda-Calculus with Sized Higher-Order Types[END_REF]) but none of them is yet available for Coq. Also the primitive pattern-matching is not the natural expected rule when dealing with elimination of a particular instance of an inductive definition, where you expect some cases to disappear or to be partially instantiated.

In systems like Coq there always has been a trade-off between keeping the language and the kernel small enough to ensure correctness and use encodings for more high-level constructions or include these constructions directly in the language.

In general the defined equality in the Calculus of Inductive Constructions does not have all the expected properties. The current work on Homotopy Type Theory [START_REF]Homotopy Type Theory Univalent Foundations of Mathematics[END_REF] is an attempt to solve this problem. It includes a notion of generalised inductive definitions where the equality definition is included in the declaration, making the definition of quotient types more direct.

Conclusions

The Calculus of Inductive Constructions provides a powerful language for the interactive development of proofs and programs. It includes a mini functional programming languages that is sufficient for programming complex data-structures and programs. The specification language itself can use a declarative style with (almost) no limit to the expressiveness. It is integrated in a proof environment (the Coq system) which provides many other functionalities like modules, libraries, notations, type inference, tactics which are essential for a practical use of the formalism. We refer the interested reader to more extensive descriptions of the system like [START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF][START_REF] Paulin-Mohring | Tools for Practical Software Verification, LASER 2011 summerschool[END_REF].

Fig. 1 .

 1 Fig. 1. Inference rules for the purely functional part of CIC

  Definition inv (x y:N) : Prop := match x,y with S _, z → ⊥ | _,_ ⇒ ⊤ end. We then can build the proof (the term I is a trivial proof of ⊤) Definition leinv n (H:le (S n) z) : ⊥ := match H in le x y return inv x y with | lez x ⇒ I | leS x y p ⇒ I end.

Fixpoints.

  Fixpoint constructions in Coq are mainly introduced via global declarations. Fixpoint f (x 1 :A 1 )... (x m :A m ){struct x n }:B:=t. they correspond to an internal fixpoint construction fix f (x 1 :A 1 )... (x n :A n ):Π(x n+1 : A n+1 ) . . . (x m : A m ),B := fun x n+1 ... x m ⇒ t.

Formally a CIC judgement will be of the form Γ ⊢ t : A with Γ a context and t and A two terms (A being also a type). The weaker judgement Γ ⊢ states that the context Γ is well-formed.The inference rules corresponding to the pure functional part of the Calculus of Constructions are given in figure1, withS def = {Prop} ∪ i∈N {Type i }. Γ ⊢ Γ ⊢ Prop : Type 1 Γ ⊢ Γ ⊢ Type i : Type i+1 Γ ⊢ x : A ∈ Γ Γ ⊢ x : A Γ ⊢ A : s x ∈ Γ s ∈ S Γ, x : A ⊢ Γ, x : A ⊢ t : B Γ ⊢ fun x : A ⇒ t : Πx : A, B Γ ⊢ f : Πx : A, B Γ ⊢ a : A Γ ⊢ f a : B[a/x] Γ, x : A ⊢ B : Prop Γ ⊢ Πx : A, B : Prop Γ, x : A ⊢ B : Type i Γ ⊢ A : Type i Γ ⊢ Πx : A, B : Type i

∃x : A, B def = ∀C : Prop, (∀x : A, B → C) → C Both the introduction and elimination rules for existential quantification in natural deduction (first column) are derivable (CIC typed terms in second column)Γ ⊢ B[t/x] Γ ⊢ ∃x : A, B Γ ⊢ p : B[t/x] Γ ⊢ fun C(H : ∀x : A, B → C) ⇒ H t p : (∃x : A, B) Γ ⊢ ∃x : A, B Γ, B ⊢ C x ∈ Γ, C Γ ⊢ C Γ ⊢ t : ∃x : A, B Γ, x : A, p : B ⊢ u : C x ∈ Γ, C Γ ⊢ t C (fun (x : A)(p : B) ⇒ u) : COne has to be careful that CIC implements a constructive logic and not a classical one. So the stronger form of elimination of absurdity namelyΓ, ¬C ⊢ ⊥ Γ ⊢ Cis not provable in general and also one can prove ∃x, B ⊢ ¬∀x, ¬B but not the opposite direction. The meaning of an existential quantification in CIC is stronger than the one in classical logic in the sense that from a proof of ∃x : A, B one will always be able to extract a term t such that B[t/x] is provable while in classical logic one only get (via Herbrand's theorem) the existence of a finite number of terms t 1 , . . . , t k such that B[t 1 /x] ∨ . . . ∨ B[t k /x] is provable for existential formulas. Higher-order quantification can also be used to represent logical relations. For instance Leibniz equality x = y with x and y of type A can be encoded using the proposition ∀P : A → Prop, P x → P y. The two rules for introduction and elimination are derivable in CIC

Proof-Theoretical Properties

The main property of the system is decidability of type-checking: we need to be able to say that a proof is correct. It requires the relation A B to be decidable, which is done by showing the system is strongly normalizing with respect to the computation rules. Another important property is to prove that any closed term with type an inductive definition will reduce to a value starting with one of the constructors of the inductive definition. Consistency can be derived as a consequence because they cannot be a proof without hypothesis of ⊥ which has no constructor.

Proof theoretical properties of systems like the Calculus of Constructions are complex to perform in full detail, first because these systems are logically powerful (due to the impredicativity, the hierarchy of universes, the type dependency) and second because there are many syntactic properties to be established like the Church-Rosser property or subject-reduction which are made even more complicated because of the general pattern of inductive definitions. Several proofs covering subsystems of Coq exists, Bruno Barras in his thesis [START_REF] Barras | Auto-validation d'un système de preuves avec familles inductives[END_REF] formalised and proved meta-theoretical properties (including typing decidability assuming normalisation) of a Calculus of Constructions with Inductive Definitions.

Pragmatic Properties

Dependent types. The type system of CIC allows types to depend on objects in many different ways. We have seen propositions parameterised by objects either defined inductively (le) or in a computational way using pattern-matching and fixpoints (inv ).

It is also possible to mix computational and logical parts. For instance one can build the type of even numbers by defining a predicate even and then introducing the type Inductive Ne : Type := Nec : Πn : N, even n → Nev.

An object in the type Ne will be a pair containing a natural number plus a proof that this number is even. This definition looks like the one for the existential quantifier given in section 2 except that it is a type and not a proposition and consequently it is possible to define a projection function of type Ne → N .

Another possibility to add logical information inside a type is to associate an index to the type declaration representing this information. A classical example is the one of vectors of length n.

Inductive vec (A:Type

We could also associate a predicate to a list describing the set of its elements, we can even use this predicate to ensure that there are no duplicate elements in the list.

Inductive L (A:Type) :

However manipulating terms in these dependent types might become tricky because the system will generally see the types vec A n and vec A m as different, even when n and m can be proven equal if they are not identical with respect to CIC internal equivalence.

Declarative specifications. Inductive definitions of relations can be used for a declarative style of specifications. They are a natural way to encode relations like reachability, or semantics of programming languages or transition systems. Proofs can be done using a resolution-like mechanism. Let us take an example. Assume we want to study a Post correspondence problem given by the three pairs of words on the alphabet {a, b}: P def = {(a, baa); (ab, aa); (bba, bb)} (example taken from Wikipedia).

We first introduce a data-type in Coq to encode words on the alphabet. We have three constructors: one for the empty word and two unary constructors to add the letter a (resp. b) in front of a word. Now a solution is given by a word x which is not empty and such that (post x x) is provable. A non-empty word can be written ax or bx. One defines the proposition which states that there exists a solution (either starting with a or with b).

Inductive sol : Prop

Now finding a solution is just finding a proof of sol. It can be done using automatic tactics. First we declare the constructors of the two definitions post and sol in the Hint database.

Hint Constructors post. Hint Constructors sol.

We can now solve the goal using an automatic tactic which tries to apply the constructors using unification and backtracking:

Lemma ok : sol. eauto 6. Defined.

The Defined command at the end builds the proof term which is type-checked by the kernel of Coq verifying that it is indeed a valid term of CIC. The term can be printed We see that the proof contains both the witness word, in this case u def = bbaabbbaa (the first b comes from the fact that the constructor solb is used), and a proof of post u u where we find the sequence 3231 corresponding to the decomposition.

Computation and Reflection

Inductive definitions help represent data-structures without extra encoding and provide primitives to define recursive functions on these data. The Coq language contains a mini ML sub-language (with no side effect and only terminating functions). It is convenient for formalising complex programs which can then be proven, the most impressive example being the CompCert project of an optimising compiler for C programs [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]. Computation is part of the Coq kernel, many efforts have been made to make it more efficient using compiler technologies.

We can use the underlying language to implement inside Coq various decision procedures. For instance we can have a concrete data structures R to represent symbolic ring expressions with variables, constants, and ring operations. The ring equality eqR can be defined using an inductive definition. Then a simplification function simpl of type R → R can be defined inside Coq and proven correct with respect to equality ∀x : R, eqR x (simpl x).

We can then prove a scheme of reflection which allows to use the result of the execution of the procedure in order to build proofs of complex facts. If we have in Coq another type C with some operations which have a Ring structure, then it is easy to define recursively a function val of type R → C which interprets a symbolic expression as an element of C, given an environment which maps variables to elements of C. We have to prove that ∀(x y : R)(ρ : X → C), eqR x y → val ρ x = val ρ y, which is just the justification that our structure C is indeed a ring.

If we put the decision procedure on R and the C interpretation together we can build a proof of ∀(x y : R)(ρ :

This lemma states the (partial)-correctness of the procedure. It is proven once but can be instantiated on many different problems.

Let us illustrate that on our ring example. We want to prove a goal of the form t = u between two Coq expressions in the concrete type C. It might require many rewriting involving associativity, commutativity, distributivity resulting is very large proof terms. Instead we take a detour via our symbolic expressions in R and then use computation. We first write a tactic which guesses by pattern-matching two symbolic expressions p and q (closed terms in R) and an environment ρ such that val ρ p ≃ t and val ρ q ≃ u. There is always at least one trivial solution with p a variable and ρ = {x → t} for the environment. But of course we want to capture in R as much structure as possible. Now the expressions simpl p and simpl q can be computed. If they happen to be the same, then val ρ (simpl x) and val ρ (simpl y) are the same Coq term v and so reflexivity justifies that val ρ (simpl x) = val ρ (simpl y). Using the correctness of the procedure we get a proof of t = u that may require a lot of computations but which corresponds to a very simple proof term correct p q ρ (eqrefl v).

This principle can be used for complex procedures but also for simple reasoning steps. The popular Ssreflect [START_REF] Gonthier | An introduction to small scale reflection in coq[END_REF] (for small scale reflection) environment (including a tactic language and libraries) which has been successfully used for formalising in Coq the four colour theorem and the Feit-Thompson theorem uses intensively this computational capability of the Coq system mainly on the type of booleans.

Proof Applications

Coq is developed for more than 30 years now and there has been a lot of impressive examples formalised using it.

Many interesting proofs combine advanced algorithms and non-trivial mathematics like the proof of the four-colour theorem by Gonthier & Werner at INRIA and Microsoft-Research [START_REF] Gonthier | Formal proof the four-color theorem[END_REF], a primality checker using Pocklington and Elliptic Curve Certificates developed by Théry et al. at INRIA [START_REF] Théry | Primality proving with elliptic curves[END_REF] and the proof of a Wave Equation Resolution Scheme by Boldo et al. [START_REF] Boldo | Formal Proof of a Wave Equation Resolution Scheme: the Method Error[END_REF]. Coq can also be used to certify the output of external theorem provers like in the work on termination tools by Contejean and others [START_REF] Contejean | A3pat, an approach for certified automated termination proofs[END_REF], or the certification of traces issued from SAT & SMT solvers done by Grégoire and others [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF]. Coq is also a good framework for formalising programming environments: the Gemalto and Trusted Logic companies obtained the highest level of certification (common criteria EAL 7) for their formalisation of the security properties of the JavaCard platform [START_REF] Chetali | About the world-first smart card certificate with EAL7 formal assurances[END_REF]; as mentioned earlier Leroy and others developed in Coq a certified optimising compiler for C (Leroy et al.) [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]. Barthe and others used Coq to develop Certicrypt, an environment of formal proofs for computational cryptography [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF]. G. Morrisett and others also developed on top of Coq the Ynot library for proving imperative programs using separation logic [START_REF] Morrisett | The Ynot project[END_REF]. These represent typical examples of what can be achieved using Coq.


Mohammed Bekkouche
email: mohammed.bekkouche@i3s.unice.fr

Hélène Collavizza

Michel Rueher
email: michel.rueher@unice.fr

LocFaults: A new flow-driven and constraint-based error localization approach *

Keywords: D.3.3 [ Language Constructs and Features]: Constraints; D.2.5 [Testing and Debugging]: Debugging aids, Diagnostics, Error handling and recovery Verification, Algorithms

We introduce in this paper LocFaults, a new flow-driven and constraint-based approach for error localization. The input is a faulty program for which a counter-example and a postcondition are provided. To identify helpful information for error location, we generate a constraint system for the paths of the control flow graph for which at most k conditional statements may be erroneous. Then, we calculate Minimal Correction Sets (MCS) of bounded size for each of these paths. The removal of one of these sets of constraints yields a maximal satisfiable subset, in other words, a maximal subset of constraints satisfying the post condition. To compute the MCS, we extend the algorithm proposed by Liffiton and Sakallah [21] in order to handle programs with numerical statements more efficiently. The main advantage of this flow-driven approach is that the computed sets of suspicious instructions are small, each of them being associated with an identified path. Moreover, the constraintprogramming based framework of LocFaults allows mixing Boolean and numerical constraints in an efficient and straightforward way. Preliminary experiments are quite encouraging.

INTRODUCTION

Error localization from counter-examples and associated execution traces is a crucial issue in the software development process. Indeed, when a program P contains errors, a model checker usually provides a counter-example and an execution trace that is too long and too difficult to understand. This kind of outputs is therefore of limited interest for the programmer who has to debug the program. Thus, identifying code portions that may contain errors is often a difficult and expensive process, even for experienced programmers.

That is why we introduce here a new flow-driven and constraint-based approach for error localization. This new approach takes advantage from the structure of the Control Flow Graph (CFG) as well as from the flexibility provided by the constraint-programming framework. The process starts with a faulty program and a counter-example violating the postcondition. To provide helpful information for finding potential errors, we generate a constraint system for the paths of the CFG for which at most k conditional statements may be erroneous. Then, we calculate Minimal Correction Sets (MCS) of bounded size for each of these paths. In other words, we bound both the number of suspected assignments on the initial path, and the number of deviations from that path. To compute MCS, we extend the algorithms introduced by Liffiton and Sakallah [START_REF] Liffiton | Algorithms for computing minimal unsatisfiable subsets of constraints[END_REF][START_REF] Liffiton | Enumerating infeasibility: Finding multiple muses quickly[END_REF] to be able to handle programs with numerical statements more efficiently. Note that LocFaults may miss some errors since the number of deviations as well as the size of the MCS are bounded to limit combinatorial explosion.

To sum up, we take advantage of the information of the CFG for computing small sets of suspicious instructions, each of them being associated to an identified path. Moreover, this constraint-programming based framework provides an efficient and straightforward way for mixing Boolean and numerical constraints.

The rest of the paper is organized as follows. Section 2 illustrates how LocFaults works on a small example. Sec-tion 3 goes into detail of the LocFaults framework. Section 4 reports experimental results on a number of benchmarks and problems, comparing our approach with BugAssist, a state-of-the art error localization framework [START_REF] Jose | Bug-assist: Assisting fault in ansi-c programs[END_REF][START_REF] Jose | Cause clue clauses: error localization using maximum satisfiability[END_REF]. Section 5 discusses related work, summarizes the contributions and presents future research directions.

MOTIVATING EXAMPLE

Consider program AbsMinus (see fig. 1). The inputs are integers {i, j} and the expected output is the absolute value of i -j. An error has been introduced in line 10, thus for the input data {i = 0, j = 1}, program AbsMinus returns -1. The postcondition here is just result = |i -j|1 .

1 class AbsMinus { 2 / * returns | i-j|,the absolute value of i minus j * / 3 / * @ ensures 4 @ ((i < j) ==> (\result == j-i)) && 5 @ ((i >= j) ==> (\result == i-j)); * / 6 int AbsMinus (int i, int j) { 7 int result;

8 int k = 0; 9 if (i <= j) { 10 k = k+2; } // error : k = k+2 instead of k=k+1 11 if (k == 1 && i != j) { 12 result = j-i; } 13 else { 14 result = i-j; } 15 return result; } } Figure 1: Program AbsMinus
The CFG of program AbsMinus and a faulty path are depicted in figure 2. This faulty path corresponds to the input data : {i = 0, j = 1}. First, LocFaults collects on path 2.(b) the constraint set C1 = {i0 = 0, j0 = 1, k0 = 0, k1 = k0 + 2, r1 = i0 -j0}2 . Then, LocFaults computes the MCS of C1. It is important to stress that the constraints defining the assignments of the input variables cannot belong to the computed MCS. Indeed, relaxing these constraints, rather corresponds to the generation of some test cases that satisfy the postcondition. So, only one MCS can be found in C1: {r1 = i0 -j0}. In other words, if we assume that the conditional statements are correct, the only suspicious statement on this faulty path is statement 14.

Then, LocFaults starts the deviation process. The first deviation (see figure 3.(a), green path) still produces a path that violates the postcondition. Thus, it is rejected. The second deviation (see figure 3.(b), blue path) produces a path that satisfies the postcondition. So, LocFaults collects the constraints on the part of path 3.(b) which precedes the deviated condition, that is C2 = {i = 0, j = 1, k0 = 0, k1 = k0 + 2}. Then LocFaults searches for an MCS of C2 ∪ ¬(k = 1 ∧ i = j).That is to say, one tries to identify the assignments which must be modified to force the program to follow a path that satisfies the postcondition. Therefore, for this second deviation two suspicious statements are identified:

• The conditional statement in line 11;

• The assignment in line 10 since the corresponding constraint is the only MCS of C2 ∪ ¬(k = 1 ∧ i = j).

Then, LocFaults goes on and tries to deviate a second condition. The only possible path is the one where both conditions of program AbsMinus are deviated. However, since it has the same prefix than the first deviated path, we discard it.

This example shows that LocFaults produces relevant and helpful information on each faulty path. Unlike to BugAssist, a state of art system, it does not merge all suspicious statements in a single set, which may be difficult to exploit by the user.

THE LocFaults FRAMEWORK

In this section we first introduce the formal definitions of MUS, MSS and MCS which are the basis of our errorlocalization framework. Then, we give an overview of BMC (Bounded Model Checking) based on constraint programming. Finally, we detail how we compute some MCS of bounded size along the program paths, using a depth-first search on the CFG of the program.

Error localization and MCS computation

Since we encode the set of statements of a faulty path as a set of constraints, the error localization problem is similar to the problem of finding a correction set for an inconsistent constraint system. This problem has been addressed both in the operational research community and constraint community. When searching useful information to correct inconsistent constraint systems, one may look for two kinds of information:

1. How many constraints in an unsatisfiable set of constraints can be satisfied ?

2. Which part of the constraint system is unsatisfiable ?

To answer these questions, the notion of MUS, MSS and MCS have been introduced by Liffiton and al [START_REF] Liffiton | Algorithms for computing minimal unsatisfiable subsets of constraints[END_REF].

A Minimal Unsatisfiable Subsets of constraints (MUS), also called "unsatisfiable cores" is an unsatisfiable system of constraints such that removing any one of its elements makes the remaining set of constraints satisfiable:

M ⊆ C is a MUS ⇔ M is UNSAT and ∀c ∈ M : M \ {c} is SAT. A Maximal Satisfiable Subset (MSS)
is a generalization of MaxSAT and MaxCSP where we consider the maximality instead of the maximum cardinality

M ⊆ C is an MSS ⇔ M is SAT and ∀c ∈ C \ M : M ∪ {c} is UNSAT.
The definition of the MSS is very close to that of IIS (Irreducible Inconsistent Subsystem) used in operational research [START_REF] Chinneck | Localizing and diagnosing infeasibilities in networks[END_REF][START_REF] Chinneck | Fast heuristics for the maximum feasible subsystem problem[END_REF][START_REF] Chinneck | Feasibility and Infeasibility in Optimization: Algorithms and Computational Methods[END_REF]]. An MCS is a subset of the constraints of an infeasible constraint system whose removal yields a satisfiable set of constraints ("correcting" the infeasibility). Furthermore it is minimal in the sense that any proper subset does not satisfy this property [START_REF] Liffiton | Algorithms for computing minimal unsatisfiable subsets of constraints[END_REF]. There is a duality relationship between the set of MUS and the set of MCS [START_REF] Birnbaum | Consistent subsets of inconsistent systems: structure and behaviour[END_REF][START_REF] Liffiton | Algorithms for computing minimal unsatisfiable subsets of constraints[END_REF] Different algorithms have been proposed for calculating IIS/MUS et MCS, e.g. Deletion Filter, Additive Method, Additive Deletion Method, Elastic Filter [START_REF] Chinneck | Localizing and diagnosing infeasibilities in networks[END_REF][START_REF] Tamiz | Detecting iis in infeasible linear programmes using techniques from goal programming[END_REF][START_REF] Chinneck | Fast heuristics for the maximum feasible subsystem problem[END_REF][START_REF] Chinneck | Feasibility and Infeasibility in Optimization: Algorithms and Computational Methods[END_REF]. Junker [START_REF] Junker | Quickxplain: Preferred explanations and relaxations for over-constrained problems[END_REF] proposed an algorithm based on a generic "Divideand-Conquer" strategy to efficiently compute IIS or MUS when the cardinality of the conflict-subsets is much smaller than the one of the whole constraint set. The algorithm introduced by Liffiton and Sakallah [START_REF] Liffiton | Algorithms for computing minimal unsatisfiable subsets of constraints[END_REF] first calculates all MCS in an increasing order, then all MUS by using the above property mentioned. The algorithm presented in section 3.4 is derived from that algorithm.

M ⊆ C is an MCS ⇔ C \ M is SAT
Various improvements of these algorithms [START_REF] Felfernig | An efficient diagnosis algorithm for inconsistent constraint sets[END_REF][START_REF] Liffiton | Enumerating infeasibility: Finding multiple muses quickly[END_REF][START_REF] Marques-Silva | On computing minimal correction subsets[END_REF] have been proposed during the last years but they are closely related to the specificity of SAT solvers, and thus, they are quite difficult to transpose to numeric constraint solvers.

Next section introduces the BMC framework we use to collect the constraints on a faulty or suspicious path.

Constraint based BMC

Constraint based BMC is a BMC approach that uses constraints for modeling the program and its specification, and constraint solving for checking if the program conforms its specification [START_REF] Collavizza | Cpbpv: a constraint-programming framework for bounded program verification[END_REF][START_REF] Collavizza | Constraint-based bmc: a backjumping strategy[END_REF]. BMC uses a bound b to unfold loops: they are replaced with conditional statements of depth b. If an error is found for a given b, then the program does not conform its specification. Otherwise, b is increased for searching a deeper error, until a maximum value of b has been reached.

Let P ROG b be the program after being unfolded b times. One BMC step checks the Hoare triplet {P RE,P ROG b ,P OST } where P RE is the precondition and P OST is the postcondition. P ROG b does not conform its specification if the formula Φ = P RE ∧ P ROG b ∧ ¬P OST is satisfiable. An instantiation of the variables of Φ is then a counter-example because it satisfies both the precondition and the program, but it does not satisfy the postcondition.

CPBPV [START_REF] Collavizza | Cpbpv: a constraint-programming framework for bounded program verification[END_REF] is a BMC tool based on constraint programming. CP BP V translates P RE and P OST into constraints, and transforms P ROG b into a CFG whose nodes are the conditions and assignments of the program translated into constraints 3 . CPBPV builds the constraint system CSP associated to formula Φ on the fly, using a depth-first search on the data structure of the graph. At the initial state, CSP contains the constraints based from P RE and ¬P OST . Then the constraints of a path are added during the graph exploration. When the last node has been reached on a path, the satisfiability of CSP is checked. When CSP has a solution, an error has been found in the program thus the BMC process is stopped. Otherwise, another branch is explored. When all the branches have been explored without finding any solution, then P ROG b is conform with its specification.

MCSs on a path

In this paper, we extend our BMC approach to locate which part of the program may be responsible for the error found during the BMC step. More precisely, let CE be a counter-example found during the BMC step. CE is the solution of CSP which contains the constraints from the precondition, the negation of the postcondition, and the constraints based on the assignments collected on the faulty path. Let P AT H denote this last set of constraints. Then the constraint system C path = CE ∪ P RE ∪ P AT H ∪ P OST is UNsatisfiable since CE is a counter-example that satisfies ¬ P OST . An MCS of C path is a set of constraints which must be removed in order to make C path satisfiable. By definition, such an MCS is a possible error localization on the faulty path. This first localization step assumes that the error is an assignment on the counter-example path. But the program can also be wrong because of a bad choice on a conditional node. LocFaults also computes bonded MCS on paths which are built by changing some conditions on the initial faulty path.

Algorithm scheme

The inputs of our algorithm are the CFG of the program, CE the counter-example, b cond , a bound on the number of conditions which are diverted and bmcs a bound on the number of MCS which are computed on each path. CE is a set of values of the input variables of the program. Roughly speaking, our algorithm traverses the CFG using CE to select one or the other branch of each conditional node, and collects the constraints associated with the assignments on the induced path. It changes zero, one or at most b cond decisions on this path. At the end of a path, the set of constraints which have been collected is unsatisfiable, and at most bmcs MCSs are computed on this CSP .

More precisely LocFaults proceeds as follows :

• It first propagates CE on the CFG until the end of the faulty path has been reached. Then it computes atmost bmcs MCSs on the current CSP . This is a first localization on the counter-example path.

• Then LocFaults tries to divert one condition. When the first conditional node cond is reached, LocFaults takes the opposite decision as the one induced by CE, and continues to propagate CE to the last CFG node.

If the CSP built from this diverted path is satisfiable, there are two kinds of suspicious error set :

the first one is the condition cond itself. Indeed, changing the decision for cond makes CE satisfies the postcondition P OST , another possible cause of the error is that a bad assignment before cond had produced a wrong decision. Thus LocFaults also computes atmost bmcs MCSs on the CSP that contains the constraints collected on the path that reaches cond.

This process is repeated on each conditional node of the counter-example path.

• A similar process is then applied for diverting k conditions for all k ≤ kmax. To increase efficiency, the conditional nodes which correct the program are marked with the number of diversions which have been made before they had been reached. For a given step k, if changing the decision of a conditional node cond marked with value k with k ≤ k corrects the program, this correction is ignored. In other words, we only consider the first time where a conditional node corrects the program.

EXPERIMENTS

To evaluate the capabilities of our approach we experimented with two sets of Benchmarks : the well known TCAS suite from Siemens [START_REF] Rosenblum | Lessons learned from a regression testing case study[END_REF], and a set of variations of the Tritype program. We compared the results of LocFaults with the one of BugAssist.

TCAS is an aircraft collision avoidance system. The program contains 173 lines of C code with almost no arithmetic operations. The suite contains 41 faulty versions .

The Tritype program is a standard benchmark in test case generation and program verification since it contains numerous non-feasible paths because of complex conditional statements in the program. The program takes three positive integers as inputs (i, j, k) the triangle sides, and returns the value 2 if the inputs correspond to an isosceles triangle, the value 3 if they correspond to an equilateral triangle, the value 1 if they correspond to some other triangle, and the value 4 otherwise. The Tritype program is also a decision problem but we derived from the initial program two versions with more arithmetic operations. The first returns the product of the length of the sides, whereas the second one computes the square of the surface of the triangle by using Heron's formula.

The results of these experiments are detailed in the next subsections. All experiments were done on an Intel Core Core i7-3720QM at 2.6 GHz with 8 GB of memory running 64-bit Linux. LocFaults uses the IBM solvers CP OPTI-MIZER and CPLEX4 .

TCAS suite

The results of the experiments are reported on Table 1. First column specifies the TCAS version number, the second one the number of errors in the program and the third column gives the number of the generated counter-examples. The two last columns provide the number of errors that have been found by LocFaults and BugAssist. Some of the versions are omitted because the errors correspond to array index out of bound and we still cannot handle this kind of overflow errors. We didn't report the computation times because there is no significant difference. The reported results for LocFaults have been obtained with at most one deviation; except for version V41 where two deviations were required.

The size of the set of suspicious instructions identified by BugAssist is in general larger than the sum of the sizes of the sets of suspicious instructions generated by LocFaults but BugAssist identifies a bit more errors than LocFaults. More importantly, since LocFaults reports a set of MCS for each faulty path, the error localization process is much more easier than with the single set of suspicious errors reported by BugAssist.

In all, the performances of LocFaults and BugAssist

Variations on the Tritype program

The results of the experiments on the different variations of the Tritype program5 are reported in Table 2. In that table, the numbers are the line numbers and the red numbers are the injected errors that have been found by the tools. For LocFaults, the underlined numbers are conditions, one line corresponds to a path through the CFG, and contains either a condition alone, or condition and the assignments before that condition which allow to change the branch. For example, for TritypeV1 in column = 1 where one condition is diverted, LocFaults first locates the condition 26 as being erroneous. Then it locates condition 48 and locates the assignments 30 or 25 which can be responsible of the bad decision on 48.

Versions 1 to 5 of Tritype correspond to the standard Tritype program where we injected different kinds of errors.

• TritypeV1 : the error was introduced in the last assignment statement of the program. LocFaults iden-tified this error in the first step, without deviating any condition.

• TritypeV2 : the error is in a nested condition, just before the last assignment. LocFaults finds the relevant suspicious statement after 4 deviations. BugAssist identifies also the relevant suspicious statement.

• TritypeV3 : the error is an assignment and will entail a bad branching. Here again, LocFaults only finds it after 4 deviations but all suspicious set contains only one statement.

• TritypeV4: the error is in a condition, at the beginning of the program. LocFaults finds it very quickly. Even the first identified suspicious statement may be helpful : it is an assignment, just after the wrong condition.

• TritypeV5 : there are two wrong conditions in this program. LocFaults needs to divert 3 conditions to find the two errors, while BugAssist only finds the first one.

• TritypeV6 : is a variation that returns the perimeter of the triangle. LocFaults identified this error in the first step, without deviating any condition.

Versions 7 and 8 of Tritype are some variations of the original program that return non linear expressions. They have the same control structure as Tritype. TritypeV7 computes the product of the three sides and TritypeV8 computes the square of the area of the triangle. The specification of TritypeV8 uses the Heron formula s(s -i)(s -j)(s -k) where s = (i + j + k)/2. To ensure that the returned value is an integer, we compute the square of the area and we assume as precondition that s is even. Moreover, the returned value varies according to the triangle type. For example, if the triangle is isosceles and i == j, the returned value is s(s -i)(s -i)(s -k), and if the triangle is equilateral, the returned value is (3 × i 4 )/16.

Computations times are very short for all programs but TritypV7 and TritypV8. Table 3 reports the times for these two programs. P stands for the pre-processing time 6 whereas the other rows contain the solving time. LocFaults is an order of magnitude faster than BugAssist on these two benchmarks. This clearly shows the benefit of using a constraint solver for programs containing non-trivial numerical statements. Indeed, these numerical constraints are much more difficult to handle by the SAT solver used in BugAssist than by the CSP solver used in LocFaults.

On all these benchmarks, the size of the set of suspicious instructions identified by BugAssist is similar to the sum of the sizes of the sets of suspicious instructions generated by LocFaults. But these benchmarks also show that the debugging process is much easier with the small set provided by LocFaults than with the global set of suspicious instructions computed by BugAssist. Our approach is a flow-based approach, that generates the sets of suspicious instructions in an incremental way. It finds errors along the path of the counter-example, and reports some explanations in an order that can help the user to find the bug. This is more appropriate for debugging than a global approach like BugAssist which computes a single set of suspicious instructions. 6 For LocFaults this is the time needed for the JDT Eclipse parser to build the AST from the Java program.

L P L = 0 ≤ 1 ≤ 2 ≤ 3
TritypeV7 0, 722s 0, 051s 0, 112s 0, 119s 0, 144s 0, 140s 20, 373s TritypeV8 0, 731s 0, 08s 0, 143s 0, 156s 0, 162s 0, 216s 25, 562s The problem of error localization was first addressed in the test community where many systems have been developed. The most famous one is Tarantula [START_REF] Jones | Visualization of test information to assist fault localization[END_REF][START_REF] Jones | Empirical evaluation of the tarantula automatic fault-localization technique[END_REF] that uses different metrics to rank suspicious statements detected while running a battery of tests. The critical point of this approach is that it requires an oracle for deciding whether the test result is correct or not. To avoid this problem, we consider here the Bounded-Model Checking (BMC) framework where we only require a postcondition or an assertion to check.

In this BMC context Bal et al [START_REF] Ball | From symptom to cause: localizing errors in counterexample traces[END_REF] developed one of the first error localization system. Roughly speaking, they perform multiple calls to a model checker and compare the trace of generated counter-examples with a correct execution trace. Transitions that are not included in the correct trace are reported as a possible cause of the error. Their algorithm has been implemented in the of SLAM BMC framework that verifies temporal safety properties of C programs.

More recently, approaches based on the derivation of correct traces were introduced in Explain [START_REF] Groce | Understanding counterexamples with explain[END_REF][START_REF] Groce | Error explanation with distance metrics[END_REF]. Explain works as follows:

1. Calling the model-checker CBMC 7 to find an execution that violates the postcondition;

2. Using a pseudo-Boolean solver for searching the nearest correct execution; Then, Explain produces a propositional formula S associated with program P but whose assignments do not violate the specification. Finally, Explain extends S with constraints defining an optimization problem the goal of which is to find a satisfying assignment that is as close as possible to the counter example; proximity is measured by a distance on the execution of P.

An approach similar to one of Explain was introduced in [START_REF] Renieris | Fault localization with nearest neighbor queries[END_REF] but it is based on testing rather than on model checking: the authors use a series of correct and incorrect tests and a distance metrics to select a correct test from a given set of test data. This approach assumes that a full oracle is available.

In [START_REF] Griesmayer | Repair of boolean programs with an application to c[END_REF][START_REF] Griesmayer | Automated fault localization for c programs[END_REF], the authors also start from a counter-example, but they use the specification to derive a correct program for the same input data. Each identified statement can be used to correct errors. This approach ensures that the errors are inside the set of suspicious statements (assuming that the error is in the considered erroneous model). In other words, their approach identifies a super set of erroneous statements. To reduce the number of potential errors, the process is restarted for various counter-examples and the intersection of the sets of suspicious statements are calculated. However, this approach suffers from two major problems:

• The search space may be very large since every expression can be modified;

• It generates numerous spurious diagnoses since any change in an expression is possible (for example, chang-ing the last assignment of a function to return the expected result).

To overcome these problems, Zhang et al [START_REF] Zhang | Locating faults through automated predicate switching[END_REF] proposed to change only predicates of the control flow. The intuition behind this approach is that by switching the results of a predicate and modifying the control flow, the program state cannot only be inexpensively modified, but in addition, it is often possible to reach a successful state. Liu et al [START_REF] Liu | Automated program debugging via multiple predicate switching[END_REF] generalized this approach by editing multiple predicates. They also propose a theoretical study of debugging algorithm for RHS errors, that is, errors in predicate control and in the right hand side of assignments.

In [START_REF] Beer | Explaining counterexamples using causality[END_REF], the authors address the problem of analyzing the trace of a counter-example and of error localization in the context of formal verification of hardware systems. They use the notion of causality introduced by Halpern and Pearl to formally define a set of causes of the violation of the specification by a counter-example.

Manu Jose and Rupak Majumdar [START_REF] Jose | Bug-assist: Assisting fault in ansi-c programs[END_REF][START_REF] Jose | Cause clue clauses: error localization using maximum satisfiability[END_REF] have addressed this problem differently: they introduced a new algorithm that uses a MAX-SAT solver to calculate the maximum number of clauses of a Boolean formula that can be satisfied by an assignment. Their algorithm works in three steps:

1. They encode a trace of a program by a Boolean formula F that is satisfiable if and only if the trace is satisfiable;

2. They build a false formula F by requiring that the postcondition is true (the formula F is unsatisfiable because the trace models a counter-example that violates the postcondition);

3. They use MAXSAT to compute the maximum number of clauses that can be satisfied in F and display the complement of this set as a potential cause of errors.

In other words, they calculate the complement of a MSS (Maximum Satisfiable Subset).

Manu Jose and Rupak Majumdar [START_REF] Jose | Bug-assist: Assisting fault in ansi-c programs[END_REF][START_REF] Jose | Cause clue clauses: error localization using maximum satisfiability[END_REF] have implemented their algorithm in BugAssist, a state-of-art verification tool based on CBMC. Si-Mohamed Lamraoui and Shin have recently developed SNIPER, a tool that generalizes the approach of BugAssist in order to improve error localization in programs with multiples faults. SNIPER calculates the MSS of a formula ψ = EI ∧ T F ∧ AS where EI encodes the erroneous input values, T F denotes a formula modelling all paths of the program, and AS is the violated assertion. The MCSs are obtained by taking the complement of the calculated MSS. The implementation is based on the intermediate representation LLVM and the SMT solver Yices. The authors compared SNIPER with BugAssist on the Siemens test suite TCAS. SNIPER identified by anywhere 5% more errors than BugAssist but required about much more times than BugAssist on this benchmark. More importantly, their approach assumes that a set of inputs that triggers all faults in the program is available.

In [START_REF] Wotawa | Automated debugging based on a constraint model of the program and a test case[END_REF], the authors propose to compute irreducible infeasible subsets of constraints. They use a constraint solver to derive the MCS from these sets but the number of single fault candidates they generate is rather large.

There are some similarities between the approach we propose here and the framework introduced by Manu Jose and Rupak Majumdar. The main differences are:

1. We use the control flow graph to collect the constraints on the path from the counter example, as well as on the derived paths from the path of the counter-example by assuming that at most k conditional statements may contain errors. So, we do not transform the whole program into a system of constraints.

2. We use more general algorithms than MAXSAT that make it easier to deal with numerical constraints.

Contribution and future work

Our flow-based and incremental approach is a good way to help the programmer with bug hunting since it locates the errors around the path of the counter-example. Further work concerns programs with loops where scalability may be an issue. We plan also to develop an interactive version of our tool that provides the localizations one after the others, and takes benefit from the user knowledge to select the condition that must be diverted.

Furthermore, the constraint-based framework that we have introduced is well adapted for handling arithmetic operations. Moreover, it can be extended in straightforward way for error-localization in programs with floating-point numbers computations. Such an extension would be more difficult in SAT-based framework of BugAssist, or in SNIPER where the whole program is transformed in anLLVM intermediate representation.

Figure 3 :

 3 Paths with one deviation -Program AbsMinus and ∀c ∈ M : (C \ M ) ∪ {c} is UNSAT.

  Various techniques to support error localisation have been proposed in the test and verification community.

7

  http://www.cprover.org/cbmc/ 3. Computing the difference between both traces.

Table 1 :

 1

	Version Nb E Nb CE	LF	BA
	V1	1	131	131 131
	V2	2	67	67	67
	V3	1	23	23	13
	V4	1	20	4	20
	V5	1	10	9	10
	V6	1	12	11	12
	V7	1	36	36	36
	V8	1	1	1	1
	V9	1	7	7	7
	V10	2	14	12	14
	V11	2	14	12	14
	V12	1	70	45	48
	V13	1	4	4	4
	V14	1	50	50	50
	V16	1	70	70	70
	V17	1	35	35	35
	V18	1	29	28	29
	V19	1	19	18	19
	V20	1	18	18	18
	V21	1	16	16	16
	V22	1	11	11	11
	V23	1	41	41	41
	V24	1	7	7	7
	V25	1	3	2	3
	V26	1	11	7	11
	V27	1	10	9	10
	V28	1	75	74	58
	V29	1	18	17	14
	V30	1	57	57	57
	V34	1	77	77	77
	V35	1	75	74	58
	V36	1	122	120 122
	V37	1	94	21	94
	V39	1	3	2	3
	V40	2	122	72	122
	V41	1	20	16	20

Results on TCAS

are very similar on this benchmark well adapted for a Boolean solver.

Table 2 :

 2 Tritype benchmark

		LocFaults	BugAssist
	Programme	P

Table 3 :

 3 Computation times for non linear programs

Specifications are written in JML http://www.eecs.ucf. edu/~leavens/JML/index.shtml

Before collecting the constraints, a variable renaming is required. More precisely, the program has to be transformed in DSA form[START_REF] Barnett | Weakest-precondition of unstructured programs[END_REF] which ensures that every variable is assigned at most once along any path.

To avoid the problem of multiple definition of variables, we use the DSA (Dynamic Single Assignment) form[START_REF] Barnett | Weakest-precondition of unstructured programs[END_REF].

http://www-01.ibm.com/software/commerce/ optimization/cplex-cp-optimizer/

The source code of these benchmarks can be found at: http://users.polytech.unice.fr/~rueher/Benchs/ LocF/

* This work was partially supported by ANR VAC-SIM (ANR-11-INSE-0004), ANR AEOLUS (ANR-10-SEGI-0013), and OSEO ISI PAJERO projects. Part of this work was done while Michel Rueher was visiting professor at NII (National Institute of Informatics), Tokyo. contribution was authored or co-authored by an employee, contractor or affiliate of the national government. As such, the Government retains a nonexclusive, royalty-free