Emmanuel Creusé
email: creuse@math.univ-lille1.fr

Mohamed Farhloul
email: mohamed.farhloul@umoncton.ca

Serge Nicaise
email: serge.nicaise@univ-valenciennes.fr

Luc Paquet
email: luc.paquet@univ-valenciennes.fr

E Creus É

A POSTERIORI ERROR ESTIMATES OF THE STABILIZED CROUZEIX-RAVIART FINITE ELEMENT METHOD FOR THE LAM É-NAVIER EQUATIONS

Keywords: Crouzeix-Raviart element, nonconforming method, stabilized method, nonlocking, a posteriori error estimates AMS subject classifications. 65N30, 65N15, 65N50

teaching and research institutions in France or abroad, or from public or private research centers.

A posteriori error estimates of the stabilized Crouzeix-Raviart finite element method for the Lamé-Navier equations

1. Introduction. The finite element methods are widely used for the numerical approximation of many problems occurring in engineering applications, like the Laplace equation, the Lamé system, etc.... (see [START_REF] Brenner | The Mathematical Theory of Finite Element Methods[END_REF][START_REF] Ciarlet | The finite element method for elliptic problems[END_REF]). In practice, adaptive techniques based on a posteriori error estimators have become indispensable tools for such methods. Hence there now exists a large number of publications devoted to the analysis of some finite element approximations of problems from solid mechanics and obtaining locally defined a posteriori error estimates. We refer to the monographs [START_REF] Ainsworth | A posteriori error estimation in finite element analysis[END_REF][START_REF] Babuška | The finite element methods and its reliability[END_REF][START_REF] Verfürth | A review of a posteriori error estimation and adaptive mesh-refinement techniques[END_REF] for a good overview on this topic.

For the elasticity system in the primal variables, several different approaches have been developed: Residual type error estimators [START_REF] Babuška | Analysis of the efficiency of an a posteriori error estimator for linear triangular elements[END_REF][START_REF] Babuška | A feedback finite element method with a posteriori error estimation. I: The finite element method and some basic properties of the a posteriori error estimator[END_REF][START_REF] Carstensen | A unifying theory of a posteriori error control for nonconforming finite element methods[END_REF][START_REF]A review of a posteriori error estimation techniques for elasticity problems[END_REF][START_REF] Wihler | Locking-free adaptive discontinuous Galerkin FEM for linear elasticity problems[END_REF][START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF], methods based on the resolution of local subproblems by using higher order elements [START_REF] Babuška | Analysis of the efficiency of an a posteriori error estimator for linear triangular elements[END_REF][START_REF] Babuška | A posteriori error estimates for the finite element method[END_REF][START_REF] Bank | Some a posteriori error estimators for elliptic partial differential equations[END_REF], averaging techniques (the so-called Zienkiewicz-Zhu estimators) [START_REF] Ainsworth | Reliable and robust a posteriori error estimation for singularly perturbed reaction-diffusion problems[END_REF][START_REF] Ainsworth | A posteriori error estimation in finite element analysis[END_REF][START_REF] Zhu | Adaptive techniques in the finite element method[END_REF][START_REF] Zienkiewicz | A simple error estimator and adaptive procedure for practical engineering analysis[END_REF] and finally estimators based on equilibrated fluxes [START_REF] Ainsworth | A posteriori error estimators for 2nd order elliptic systems II. an optimal order process for calculating self-equilibrated fluxes[END_REF][START_REF] Brink | A posteriori error estimation in large-strain elasticity using equilibrated local Neumann problems[END_REF][START_REF] Ladevèze | Accuracy of elastoplatic and dynamic analysis[END_REF][START_REF] Ladevèze | Error estimate procedure in the finite element method and applications[END_REF][START_REF] Ladevèze | Error estimates and mesh optimization for finite element computation[END_REF][START_REF] Nicaise | An a posteriori error estimator for the Lamé equation based on equilibrated fluxes[END_REF]. For methods based on dual variables, like mixed methods, we refer to [START_REF] Carstensen | A posteriori error estimates for mixed FEM in elasticity[END_REF][START_REF] Carstensen | Locking-free adaptive mixed finite element methods in linear elasticity[END_REF][START_REF]A posteriori error control in low-order finite element discretisations of incompressible stationary flow problems[END_REF][START_REF] Boulaajine | A posteriori error estimation for the dual mixed finite element method of the elasticity problem in a polygonal domain[END_REF][START_REF] Houston | An hp-adaptive mixed discontinuous Galerkin FEM for nearly incompressible linear elasticity[END_REF]; note that such methods are usually locking free and therefore the obtained estimators are usually locking free.

Here we analyze two displacement methods based on the primal variables variant of the ones introduced by P. Hansbo and M.G. Larson in [START_REF] Hansbo | Discontinuous Galerkin and the Crouzeix-Raviart element: application to elasticity[END_REF] which are nonconforming methods based on the Crouzeix-Raviart finite element. These methods are locking free and very cheap. In [START_REF] Hansbo | Discontinuous Galerkin and the Crouzeix-Raviart element: application to elasticity[END_REF], the authors derive a priori optimal error estimates uniform in the Lamé parameter λ (see Theorem 3.1 of [START_REF] Hansbo | Discontinuous Galerkin and the Crouzeix-Raviart element: application to elasticity[END_REF]). In this paper, we propose an a posteriori error analysis of these methods. Our analysis enters in the family of estimators of residual type since our error indicator is based on residuals on each triangle and jumps across the inter-element boundaries. We prove reliability of the indicator uniformly in λ (and h), in particular avoiding locking phenomena. The proof is based on a discrete divergence stability result (see [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF] for another scheme), the use of an appropriate decomposition of the error into continuous and discontinuous parts [START_REF] Houston | Mixed discontinuous Galerkin approximation of the Maxwell operator: Non-stabilized formulation[END_REF]. Local efficiency of our indicator follows by using classical inverse estimates, the use of a strengthened norm allows to obtain its robustness.

Note that our methods enter in a similar framework than the ones in [START_REF] Carstensen | A unifying theory of a posteriori error control for nonconforming finite element methods[END_REF][START_REF] Wihler | Locking-free adaptive discontinuous Galerkin FEM for linear elasticity problems[END_REF][START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF]. But our upper bound cannot be deduced from [START_REF] Carstensen | A unifying theory of a posteriori error control for nonconforming finite element methods[END_REF] because the assumption (2.12) from that paper is not satisfied by our scheme. On the other hand, the schemes in [START_REF] Carstensen | A unifying theory of a posteriori error control for nonconforming finite element methods[END_REF][START_REF] Wihler | Locking-free adaptive discontinuous Galerkin FEM for linear elasticity problems[END_REF][START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF] are different from our proposed schemes, nevertheless the proof of the upper bound uses similar arguments than in [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF].

The outline of the paper is as follows: We recall in Section 2 the boundary value problem and its numerical approximation. Section 3 is devoted to the proof of the discrete divergence stability result. The proof of the upper error bound is made in section 4; and the lower bound is obtained in section 5. Finally some numerical tests that confirm our theoretical results are presented in the last section.

Let us finish this introduction with some notations used in the remainder of the paper: On D, the L 2 (D)-norm will be denoted by • D . The usual norm and seminorm of H s (D) (s ≥ 0) are denoted by • s,D and | • | s,D , respectively. In the case D = Ω, the index Ω will be omitted. Similar H(div, Ω) is defined by

H(div, Ω) = {v ∈ L 2 (Ω) 2 : div v ∈ L 2 (Ω)},
equipped with its natural norm. Finally, the notation a b means the existence of a positive constant C, which is independent of the mesh size, of the considered quantities a and b and of the Lamé coefficient λ such that a ≤ Cb. In other words, the constant only depends on the aspect ratio of the mesh, on the domain Ω and on the shear modulus µ, but not on Lamé coefficient λ (see below).

A discontinuous

Galerkin method for the elasticity system.

The boundary value problem of elasticity.

Let Ω be a plane domain with a polygonal boundary. More precisely, we assume that Ω is a simply connected domain and that its boundary Γ is the union of a finite number of linear segments Γ j , 1 ≤ j ≤ n e (Γ j is assumed to be an open segment). In this domain, we consider an elastic isotropic material. Let u = (u 1 , u 2 ) be the displacement field and f = (f 1 , f 2 ) ∈ [L 2 (Ω)] 2 the body force by unit of mass. For simplicity, we consider in Ω the pure homogeneous displacement problem. Thus the displacement field u = (u 1 , u 2 ) satisfies the following equations and boundary condition:

-div σ(u) = f in Ω, u = 0 on Γ, (2.1)
where the stress tensor is defined by

σ(u) := 2µ (u) + λ tr (u)I. (2.
2)

The positive constants µ and λ are called the Lamé coefficients where µ ≡ G is the shear modulus ( [START_REF] Parton | Mathematical methods of the theory of elasticity[END_REF], p. 207) ( [START_REF] Frey | Analyse des Structures et Milieux Continus Mécanique des Solides[END_REF], pp. 72-75, 57-58). We assume that [START_REF] Brenner | The Mathematical Theory of Finite Element Methods[END_REF] (λ, µ)

∈ [λ 0 , +∞[×[µ 1 , µ 2 ] (2.3)
where 0 < µ 1 < µ 2 and λ 0 > 0.

As usual, (u) denotes the linearized strain tensor, i.e., (u) :=

find u ∈ H 1 0 (Ω) 2 such that Ω σ(u) : (v) dx = Ω f • v dx, ∀v ∈ H 1 0 (Ω) 2 , (2.4)
where σ : denotes the contraction of the two tensors, i.e.,

σ : = 2 i,j=1 σ ij ij .
The existence and uniqueness of the solution in (2.4), for a given

f ∈ H -1 (Ω) 2 ,
follows from the first Korn inequality (cf. [START_REF] Brenner | The Mathematical Theory of Finite Element Methods[END_REF], p.286). In the following, we suppose that f ∈ L 2 (Ω) 2 .

2.2. The discontinuous Galerkin methods. In order to formulate the discrete problems introduced by P. Hansbo and M.G. Larson in [START_REF] Hansbo | Discontinuous Galerkin and the Crouzeix-Raviart element: application to elasticity[END_REF], we first recall some notation.

Let (T h ) h>0 , be a regular family of triangulations. Let us fix a triangulation T h ∈ (T h ) h>0 and let E h denote the set of all edges of the triangulation T h . We split E h into two disjoint subsets: E I h the subset of edges contained in Ω and E ∂ h the subset of edges contained in the boundary of Ω. Further, with each edge E, we associate a fixed unit normal n E such that for edges contained in ∂Ω, n E is the exterior unit normal; we further fix a unit tangent t E so that {n E , t E } forms an orthonormal basis of R 2 . For any edge E and any triangle T , we denote by |E| the length of E and |T | the area of T .

Let

DF (T h ) := {v h ∈ L 2 (Ω) 2 ; ∀T ∈ T h : v h|T ∈ [P 1 (T )] 2 }
be the space of piecewise linear discontinuous functions (as usual P 1 (T ) denotes the space of polynomials of degree less than or equal to 1 on T ). For a function v h ∈ DF (T h ) we denote its jump at an edge

E by [[v h ]] E = v + h -v - h for E ∈ E I h and [[v h ]] E = v + h for E ∈ E ∂ h , and the average v h E = (v + h + v - h )/2 for E ∈ E I h and v h E = v + h for E ∈ E ∂ h , where v ± h (x) = lim h→0 + v h (x ∓ hn E ) with x ∈ E.
In the same spirit, we define its broken strain tensor h (v h ) by

h (v h ) T = (v h|T ) ∀T ∈ T h ,
its broken stress tensor σ h (v h ) and broken divergence div h v h is defined similarly. We further introduce the Crouzeix-Raviart space of vector fields CR (T h ):

CR (T h ) := {v h ∈ L 2 (Ω) 2 ; ∀T ∈ T h : v h|T ∈ [P 1 (T )] 2 , [[P 0 v h ]] E = 0, ∀E ∈ E h } (2.5)
where for any edge E and any w ∈ L 2 (E)

P 0 w := 1 |E| E wds,
and therefore

[[P 0 v h ]] E := P 0 [[v h ]] E = 1 |E| E v + h ds - 1 |E| E v - h ds.
The first discontinuous Galerkin method is a variant of the one introduced in [20] and reads as follows: find

u h ∈ DF (T h ) such that a h (u h , v h ) = (f, v h ), ∀v h ∈ DF (T h ) .
(2.6)

The bilinear form is here defined by

a h (u h , v h ) := a 0h (u h , v h ) + (2µ + λ)λγ 0 E∈E h 1 h E ([[P 0 u h • n E ]] , [[P 0 v h • n E ]]) E (2.7) +2µγ 0 E∈E h 1 h E ([[P 0 u h • t E ]] , [[P 0 v h • t E ]]) E - E∈E h (( σ h (u h ) E n E , [[v h ]] E ) E + ( σ h (v h ) E n E , [[u h ]] E ) E ) , a 0h (u h , v h ) := T ∈T h (σ(u h ), (v h )) T + 2µγ 1 E∈E h 1 h E ([[u h ]] , [[v h ]]) E , (2.8)
while the linear form is defined by

(f, v h ) = Ω f • v h dx.
Here the parameters γ 0 , γ 0 and γ 1 are the stabilizing parameters fixed below.

Here and below (σ

(u h ), (v h )) T means the L 2 -inner product T σ(u h ) : (v h ) dx.

Similarly for vector valued functions

v, w ∈ L 2 (E) 2 , (v, w) E means the L 2 -inner prod- uct E v • w ds.
Note that our bilinear form a h differs from the one in [START_REF] Hansbo | Discontinuous Galerkin and the Crouzeix-Raviart element: application to elasticity[END_REF] by the second and third terms of the right-hand side of (2.7), indeed in that paper these two terms are replaced by

(2µ + λ)γ 0 E∈E h 1 h E ([[P 0 u h ]] , [[P 0 v h ]]) E .
This modification is made to have a discrete stability result and hence a robust a posteriori estimate that cannot be obtained if we keep the original term from [START_REF] Hansbo | Discontinuous Galerkin and the Crouzeix-Raviart element: application to elasticity[END_REF]. Note further that the bilinear form a h is similar to the one in [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF] except that the second and third terms are replaced by

λ 2 γ 0 E∈E h 1 h E ([[u h • n E ]] , [[v h • n E ]]) E .
As a consequence the well-posedness of the corresponding problem in [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF] is obtained for γ 1 and γ 0 large enough (independently of λ), while our problem is well-posed only for γ 0 and γ 0 large enough (independently of λ). Our approach allows then to use a penalization parameter γ 1 as small as we want (but bounded away from zero). This difference also implies the use of a different error norm.

The well-posedness of problem (2.6) follows from the strong coerciveness of a h in DF (T h ), that we now show (see Proposition 2.2 of [START_REF] Hansbo | Discontinuous Galerkin and the Crouzeix-Raviart element: application to elasticity[END_REF] or Proposition 2.2 of [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF]) Proposition 2.1. There exist three positive constants γ min , γ min and C independent of λ, µ and the mesh size h such that for all γ 0 > γ min and all γ 0 > γ min and any v h ∈ DF (T h ), we have

a h (v h , v h ) ≥ C 2µ h (v h ) 2 + λ div h v h 2 + (2µ + λ)λ E∈E h 1 h E [[P 0 v h • n E ]] 2 E + 2µ E∈E h 1 h E [[P 0 v h • t E ]] 2 E + 2µγ 1 E∈E h 1 h E [[v h ]] 2 E Proof.
First for an arbitrary edge E, we have

( σ h (v h ) E n E , [[v h ]] E ) E = 2µ( (v h ) E n E , [[v h ]] E ) E + λ([[div h v h ]] , [[v h • n E ]] E ) E ,
and since h (v h ) and div h v h are piecewise constant, we get

( σ h (v h ) E n E , [[v h ]] E ) E = 2µ( (v h ) E n E , [[P 0 v h ]] E ) E +λ([[div h v h ]] , [[P 0 v h • n E ]] E ) E .
By Cauchy-Schwarz's and Young's inequalities we obtain

|( σ h (v h ) E n E , [[v h ]] E ) E | ≤ µ δ h E (v h ) E 2 E + µδ h -1 E [[P 0 v h ]] E 2 E + λ 2(2µ + λ)δ h E [[div h v h ]] E 2 E + λ(2µ + λ)δ 2 h -1 E [[P 0 v h • n E ]] E 2 E .
for any δ, δ > 0. Using the regularity assumption of the mesh, there exists a positive constant C tr such that

h E [[div h v h ]] E 2 E ≤ C tr div h v h 2 ω E , h E (v h ) E 2 E ≤ C tr h (v h ) 2 ω E ,
where, as usual, ω E is the patch associated with E, i.e., ω E = T + E ∪ T - E , when E is the common edge between T + E and T - E . These estimates in the previous one lead to

E∈E h ( σ h (v h ) E n E , [[v h ]] E ) E ≤ 2µC tr δ h (v h ) 2 + µδ E∈E h h -1 E [[P 0 v h ]] E 2 E + λC tr (2µ + λ)δ div h v h 2 + λ(2µ + λ)δ 2 E∈E h h -1 E [[P 0 v h • n E ]] E 2 E .
By this estimate and the definition of a h , we deduce that

a h (v h , v h ) ≥ 2µ(1 - 2C tr δ ) h (v h ) 2 + λ(1 - 2C tr (2µ + λ)δ ) div h v h 2 + 2µγ 1 E∈E h 1 h E [[v h ]] E 2 E + (2µ + λ)λ γ 0 -δ - 2µδ (2µ + λ)λ E∈E h 1 h E [[P 0 v h • n E ]] 2 E + 2µ(γ 0 -δ ) E∈E h 1 h E [[P 0 v h • t E ]] E 2 E .
Now we choose δ and δ such that

(1 - 2C tr δ ) = (1 - 2C tr (2µ + λ)δ ) = 1 2 ,
or equivalently δ = 4C tr and δ = 4C tr (2µ + λ) .

With this choice we then have

a h (v h , v h ) ≥ µ h (v h ) 2 + λ 2 div h v h 2 + 2µγ 1 E∈E h 1 h E [[v h ]] E 2 E + (2µ + λ)λ γ 0 - 4C tr (2µ + λ) - 8µC tr (2µ + λ)λ E∈E h 1 h E [[P 0 v h • n E ]] 2 E + 2µ(γ 0 -4C tr ) E∈E h 1 h E [[P 0 v h • t E ]] E 2 E .
The conclusion follows with the choice

γ min = max{1, 4C tr (2µ + λ) + 8µC tr (2µ + λ)λ
} and γ min = 4C tr .

By the previous result, we deduce that for γ 0 > γ min and γ 0 > γ min , problem (2.6) is well posed.

As shown in Proposition 2.1 of [START_REF] Hansbo | Discontinuous Galerkin and the Crouzeix-Raviart element: application to elasticity[END_REF] the method is consistent, namely

a h (u -u h , v h ) = 0, ∀v h ∈ DF (T h ) .
(2.9)

Restricting the discontinuous Galerkin method to the space of Crouzeix-Raviart functions, we obtain the following simplified scheme: find u 0h ∈ CR (T h ) such that

a 0h (u 0h , v h ) = (f, v h ), ∀v h ∈ CR (T h ) .
(2.10)

As before this second method is consistent:

a 0h (u -u 0h , v h ) = 0, ∀v h ∈ CR (T h ) . (2.11)
Observe that Theorem 2.3 of [START_REF] Nicaise | About the Lamé system in a polygonal or a polyhedral domain and a coupled problem between the Lamé system and the plate equation. I. Regularity of the solutions[END_REF] guarantees that the displacement vector field u ∈ H 3/2+ (Ω)

2 for some ∈]0, 1 2 [. Consequently σ(u)

• n E has sense on each edge

E ∈ E h as an element of [H (E)] 2 ⊂ L 2 (E)
2 and Green's formula can be applied element by element. Hence the consistency always holds.

We finally refer to [START_REF] Hansbo | Discontinuous Galerkin and the Crouzeix-Raviart element: application to elasticity[END_REF] for robust a priori error estimates.

Our goal is to bound the "triple norm" |||e||| := a 0h (e, e) of the error

e := u -u h .
But in order to get a robust estimate we even need to use the parameter depending norm:

|||e||| 2 λ = |||e||| 2 + λ 2 Π 0 div h e 2 + λ 2 E∈E h 1 h E [[P 0 e • n E ]] 2 E ,
where div h e means the broken divergence and Π 0 is the L 2 -projection on L 2 0 (Ω) 2 defined by

Π 0 f = f - 1 |Ω| Ω f (x) dx, ∀f ∈ L 2 (Ω) 2 .
Before going on notice that if u 0h ∈ CR (T h ), then

Ω div h u 0h dx = 0.
3. Discrete stability. The stability of the continuous problem (2.4) was proved in Proposition 3.2 of [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF] and means that there exists a positive constant c independent of λ such that

λ div u ≤ c f .
A discrete version of this estimate was also proved in Corollary 3.7 of [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF] for their own scheme. Using similar arguments we also obtain a discrete stability.

Proposition 3.1. If u h ∈ DF (T h ) is the solution of (2.6), then

|||u h ||| λ f .
Proof. We first use Lemma 3.5 of [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF] that yields w ∈ DF (T h ) ∩ H(div, Ω) such that div w = -λΠ 0 (div h u h ),

∇ h w λ Π 0 (div h u h ) , E∈E h 1 h E [[w]] 2 E λ 2 Π 0 (div h u h ) 2 .
With such a choice we notice that in a h (u h , w) the term

(2µ + λ)λγ 0 E∈E h 1 h E ([[P 0 u h • n E ]] , [[P 0 w • n E ]]) E ,
is zero and therefore the arguments of Proposition 3.6 of [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF] can be applied.

4.

Robust upper bound of the error. For all T ∈ T h , the local estimator η T is defined by

η 2 T = h 2 T f T 2 T + E∈E h :E⊂T h E [[σ(u h ) • n E ]] E 2 E + E∈E h :E⊂T 1 h E ( [[u h ]] 2 E +λ 2 [[P 0 u h • n E ]] 2 E ),
where

f T = 1 |T | T f (x) dx.
The global estimator is given by

η 2 = T ∈T h η 2 T .
Finally let

osc 2 (f ) = T ∈T h h 2 T f -f T 2 T
be the oscillating term. Now we are able to state our locking-free a posteriori error estimate: Theorem 4.1. With the previous notation, we have the following a posteriori estimate:

|||e||| λ η + osc(f ). (4.1)
Proof. We proceed as in the proof of Theorem 4.2 of [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF]. Namely we take

ω ∈ H 1 0 (Ω) 2 such that div ω = λΠ 0 (div h e), ω 1,Ω λ Π 0 (div h u h ) ,
and such that there exist β > 0 and κ > 0 for which 4µ (e c ) 2 + λ 2 Π 0 (div h e) 2 ≤ κ(2µ( (e c ), (e c + βω)) + βλ(div h e, div ω)),(4.2)

where, as usual (see for instance [START_REF] Houston | Mixed discontinuous Galerkin approximation of the Maxwell operator: Non-stabilized formulation[END_REF][START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF]), e c is the continuous part of the error, namely

e c = u -u c h , and
u h = u c h + u ⊥ h , with u c h ∈ V c h := DF (T h ) ∩ H 1 0 (Ω) 2 and u ⊥ h ∈ DF (T h ) ⊥ ,
where DF (T h ) ⊥ is an appropriate orthogonal complement of V c h into DF (T h ). In a first step using this splitting and the standard estimate

∇ h u ⊥ h 2 E∈E h 1 h E [[u h ]] 2 E , (4.3)
we have (compare with the estimate (29) from [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF])

|||e||| 2 λ (e c ) 2 + λ 2 Π 0 (div h e) 2 (4.4)
+ E∈E h 1 h E ( [[u h ]] 2 E + λ 2 [[P 0 u h • n E ]] 2 E ).
Hence it remains to estimate the first two terms of this right-hand side. For that purpose, we use (4.2) and transform its right-hand side as in [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF] to get 4µ (e c ) 2 + λ 2 Π 0 (div h e) 2 (σ(u), (w)) -(σ h (u h ), (w)) (4.5) +2µ( (u ⊥ h ), (w)) -λ(div h e, div e c ), where w = e c + βω that belongs to H 1 0 (Ω) 2 and satisfies (see [11, p. 1550])

w 1,Ω |||e||| λ (4.6)
For the two first terms of this right-hand side we use the continuous and discrete formulation to get successively (with w h = I Cl (w) the Clément interpolant of w)

(σ(u), (w)) -(σ h (u h ), (w)) = (σ(u), (w -w h )) -(σ h (u h ), (w -w h )) + (σ(u), (w h )) -(σ h (u h ), (w h )) = (σ(u), (w -w h )) -(σ h (u h ), (w -w h )) - E∈E h ( σ(w h ) E n E , [[u h ]] E ) E .
Hence using again the continuous formulation and piecewiese Green's formula, we arrive at

(σ(u), (w)) -(σ h (u h ), (w)) = (f, w -w h ) - E∈E h (([[σ h (u h ) • n E ]] , w h ) E + ( σ(w h ) E n E , [[u h ]] E ) E ) .
The first term is estimated in a standard way. The second term is also estimated in a classical way, namely

E∈E h ([[σ h (u h ) • n E ]] , w h ) E = E∈E h ([[σ h (u h ) • n E ]] , w h -w) E ,
and therefore by classical local error estimates on the Clément interpolant ([29], Lemma 1.4, p. 11) using Lemma 3.4 of [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF], we get

E∈E h ([[σ h (u h ) • n E ]] , w h ) E η w 1,Ω .
For the last term we can write (see above)

( σ(w h ) E n E , [[u h ]] E ) E = 2µ( (w h ) E n E , [[u h ]] E ) E + λ( div h w h E , [[P 0 u h • n E ]] E ) E .
Hence using scaling arguments, we obtain

E∈E h ( σ(w h ) E n E , [[u h ]] E ) E w h 1,Ω E∈E h 1 h E [[u h ]] 2 E + λ 2 [[P 0 u h • n E ]] 2 E 1 2
.

Hence using again Lemma 1.4 of [START_REF] Verfürth | A review of a posteriori error estimation and adaptive mesh-refinement techniques[END_REF], we get

E∈E h ( σ(w h ) E n E , [[u h ]] E ) E η w 1,Ω .
The third term of (4.5) is estimated by using (4.3), namely

|2µ( (u ⊥ h ), (w))| ∇ h u ⊥ h ∇w η ∇w .
For the last term of (4.5) since e c belongs to H 1 0 (Ω) 2 its divergence is of mean zero and therefore as in [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF], we find

-λ(div h e, div e c ) ≤ -λ(div h e, div h u ⊥ h ).
Hence by Cauchy-Schwarz's inequality and the estimate (4.3), we again arrive at -λ(div h e, div e c ) ηλ div h e η |||e||| λ .

All the previous estimates lead to the conclusion.

5.

Lower bound of the error. For a subset ω of Ω, we denote by

|||e||| 2 λ,ω := (σ h (e), h (e)) ω + λ 2 Π 0 div h e 2 ω + E∈E h :E⊂ω 1 h E 2µγ 1 [[u h ]] 2 E + λ 2 [[P 0 u h • n E ]] 2 E , osc 2 ω (f ) := T ∈T h :T ⊂ω h 2 T f -f T 2 T .
As usual, for any triangle T we denote by

ω T = ∪ T ∈T h :T ∩T =∅ T ,
the patch associated with T . Similarly for an edge E, we set

ω E = ∪ T ∈T h :E⊂T T .
We start with the element residual. Lemma 5.1. For all T ∈ T h , we have

h T f T T |||e||| λ,T + osc T (f ).
Proof. If b T is the standard bubble function associated with T , we set w T = f T b T . Hence by a standard inverse inequality we have

f T 2 T T f T • w T dx = T (f T -f ) • w T dx - T div σ(u -u h ) • w T dx,
reminding that div σ(u) = -f . For the second term of this right-hand side applying Green's formula we obtain

f T 2 T T (f T -f ) • w T dx + T σ(u -u h ) : (w T ) dx.

Now we can write

T σ(u -u h ) : (w T ) dx = 2µ T (u -u h ) : (w T ) dx + λ T div(u -u h ) div(w T ) dx = 2µ T (u -u h ) : (w T ) dx + λ Ω div h (u -u h ) div(w T ) dx.
Since w T can be seen as a function in

H 1 0 (Ω) 2 , we deduce that T σ(u -u h ) : (w T ) dx = 2µ T (u -u h ) : (w T ) dx + λ Ω Π 0 div h (u -u h ) div(w T ) dx = 2µ T (u -u h ) : (w T ) dx + λ T Π 0 div h (u -u h ) div(w T ) dx.
By Cauchy-Schwarz's inequality and the inverse inequality (w

T ) T h -1 T f T T , we obtain h T f T T osc T (f ) + (u -u h ) T + λ Π 0 div h (u -u h ) T .
The conclusion follows from the direct estimate (e) 2 T ≤ 1 2µ T σ(e) : (e) dx.

(

We argue in a similar manner for the normal jump, namely we have the Lemma 5.2. For all E ∈ E h , we have

h 1/2 E [[σ(u h ) • n E ]] E E |e| λ,ω E + osc ω E (f ).
Proof. Denoting by b E the edge bubble we set

w E = [[σ(u h ) • n E ]] E b E that belongs to [H 1 0 (ω E )] 2 .
Hence by a standard inverse inequality we have

[[σ(u h ) • n E ]] E 2 E ∼ E [[σ(u h ) • n E ]] E • w E ds = E [[σ(u h -u) • n E ]] E • w E ds = T ∈T h :T ⊂ω E ∂T σ(u h -u) • n • w E ds.
Hence an integration by parts yields

[[σ(u h ) • n E ]] E 2 E ∼ T ∈T h :T ⊂ω E ( T σ(u h -u) : ∇(w E ) dx + T f • w E dx).
Using the same argument as before and Cauchy-Schwarz's inequality and inverse inequalities we obtain

h 1/2 E [[σ(u h ) • n E ]] E E T ∈T h :T ⊂ω E ( (u h -u) T + h T f T T ) + λ Π 0 div h (u -u h ) ω E + osc ω E (f ).
The conclusion follows from Lemma 5.1 and the estimate (5.1). These two lemmas directly yield the Theorem 5.3. For all T ∈ T h , we have

η T |||e||| λ,ω T + osc ω T (f ).
6. The nonconforming Galerkin method based on the Crouzeix-Raviart element. The arguments of the three previous section can be directly applied to the discontinuous method (2.10). They are even simpler because [[P 0 u h • n]] E = 0 on any edge E. Hence we have not to use the extra term

λ 2 E∈E h 1 h E [[P 0 e • n]] 2 E .
in the norm of the error (because it is zero). More precisely we can prove the next results: Theorem 6.1. We have the following a posteriori estimate:

|||e||| + λ Π 0 div h e η 0 + osc(f ), (6.1)
where

η 2 0 = T ∈T h η 2 0T ,
and for all T ∈ T h , the local estimator η 0T is defined by

η 2 0T = h 2 T f T 2 T + E∈E h :E⊂T h E [[σ(u h ) • n E ]] E 2 E + E∈E h :E⊂T 1 h E [[u h ]] 2 E .
Theorem 6.2. For all T ∈ T h , we have

η 0T |||e||| ω T + λ Π 0 div h (e) ω T + osc ω T (f ),
where

|||e||| 2 ω := T ∈T h :T ⊂ω (σ(e), (e)) T + 2µγ 1 E∈E h :E⊂ω 1 h E [[u h ]] 2 E .
Theorem 6.1 is also a consequence of Theorem 2.1 of [START_REF] Carstensen | Averaging technique for a posteriori error control in elasticity. III. Locking-free nonconforming FEM[END_REF] since u 0h satisfies the assumptions of this theorem. We give here an alternative proof.

7. Numerical experiments. In this section, some numerical experiments are performed to illustrate the above theoretical results, similarly to the ones proposed in [START_REF] Bridgeman | Stability and a posteriori error analysis of discontinuous Galerkin methods for linearized elasticity[END_REF]. In all the following cases, Crouzeix-Raviart finite elements CR (T h ) defined by (2.5) are used on a regular mesh composed of triangles.

7.1. Divergence-free smooth solutions. The first test consists in solving equation (2.1) on the unit square Ω = (0, 1) 2 , for the exact solution given by : u(x, y) = 1 π 2 (sin(πx) sin(πy)) n-1 sin(πx) cos(πy) -sin(πy) cos(πx) ,

where n ≥ 2 is a given integer and where f is chosen accordingly. It should be noted that u is smooth, divergence-free, and that u |∂Ω = 0.

For the first example, we set n = 2. We plot in Figure 7.1 the convergence rates of the error (Figure 7.1 (a)) and of the estimator (Figure 7.1 (b)) for several values of λ, using a uniform mesh refinement strategy. It can be observed a good convergence towards zero for both of them corresponding to the one theoretically expected (namely, order 1 in h corresponding to order -1/2 in the total number of degrees of freedom ndof ). Then, the effectivity index defined by :

I ef f = η 0 |||e||| + λ Π 0 div h e
is plotted in Figure 7.2. First, it can be observed that for a given value of λ, the reliability of the estimator is ensured, as underlined by Theorem 6.1. Moreover, even if the value of I ef f is not totally independant of λ, it remains in a reasonable range (in the order of 1).

For the second example, we set n = 25 in order to generate high gradients in the vicinity of the mid-point ( 12 , 1 2 ). Consequently, instead of a uniform one, a local refinement mesh strategy is performed based on the local error estimator efficiency proven in Theorem 6.2. Here, this local refinement ensures that the mesh remains conform (there is no hanging-nodes creation), as well as regular (the minimal angle allowed in the triangulation is specified, in order to preserve the shape regularity of the mesh). We refer to [START_REF] Verfürth | A review of a posteriori error estimation and adaptive mesh-refinement techniques[END_REF] for further details and for the algorithm description (red, green and blue refinement). The resulting meshes obtained for iteration steps 1, 4 and 7 corresponding to λ = 10 4 are displayed in Figure 7.3, so that we can observe that the high gradients area is well tracked by the remeshing process. The convergence rates of the error and of the estimator are plotted in Figure 7.4 and the effectivity index in Figure 7.5. Once again, the conclusions are the same than for the first example: Experimental convergence rates of order 1 and robustness with respect to large values of λ, as well as only a small variation in λ of the effectivity index (around 1) for all the considered values of λ. In that case, the exact solution exhibits a singular behaviour around the origin. We want to check if the mesh is correctly refined around the singularity when the estimator is used to carry out the refinement process, and in the same time if the global estimator decreases consequently towards zero. The resulting meshes obtained for iteration steps 1, 7 and 10 corresponding to λ = 10 4 are displayed in Figure 7.6, and we can see that the mesh is automatically refined around the singularity. Moreover, Figure 7.7 shows that the estimator converges towards zero, with experimental convergence rates of order 1.

Fig. 7 . 1 .

 71 Fig. 7.1. Error (a) and Estimator (b) convergence rates in ndof for the regular solution, n = 2, λ from 1 to 10 4 .

13

 13

Fig. 7 . 2 .

 72 Fig. 7.2. Effectivity index I ef f for the regular solution, n = 2, λ from 1 to 10 4 .

Fig. 7 . 3 . 7 . 2 .= x 2 +

 73722 Fig. 7.3. Mesh refinements 1, 4 and 7 for the regular solution, n = 25, λ = 10 4 .

Fig. 7 . 4 .

 74 Fig. 7.4. Error (a) and Estimator (b) convergence rates in ndof for the regular solution, n = 25, λ from 1 to 10 4 .

Fig. 7 . 5 .

 75 Fig. 7.5. Effectivity index I ef f for the regular solution, n = 25, λ from 1 to 10 4 .

Fig. 7 . 6 .

 76 Fig. 7.6. Mesh refinements 1, 7 and 10 for the singular solution, λ = 10 4 .

2 Fig. 7 . 7 .

 277 Fig. 7.7. Estimator convergence rate in ndof for the singular solution, λ from 1 to 10 4 .

  1 2 (∇u + (∇u)T ) and I the identity tensor. For any tensor τ (of order 2), the trace of τ is tr τ := τ 11 + τ 22 , and

	div τ := (	∂τ 11 ∂x 1	+	∂τ 12 ∂x 2	,	∂τ 21 ∂x 1	+	∂τ 22 ∂x 2	)
	(in an orthogonal cartesian frame). The classical variational formulation of the bound-
	ary value problem (2.1) is the following:


Claire Dross
email: dross@adacore.com

Jean-Christophe Filliâtre
email: filliatr@lri.fr

Yannick Moy
email: moy@adacore.com

Correct

Correct Code Containing Containers

Keywords: containers, iterators, verification by contracts, annotations, axiomatization, API usage verification, SMT, automatic provers

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Containers are generic data structures offering a high-level view of collections of objects, while guaranteeing fast access to their content to retrieve or modify it. The most common containers are lists, vectors, sets and maps, which are usually defined in the standard library of languages, like in C++ STL, Ada Standard Libraries or Java JCL, and sometimes even as language elements, like sets in SETL [START_REF] Schwarz | Programming with sets: an introduction to SETL[END_REF] or maps in Perl. In critical software where verification objectives severely restrict the use of pointers, containers offer an attractive alternative to pointer-intensive data structures. Containers offer both a better defense against errors than low-level code manipulating pointers, and a rich high-level API to express properties over data. This is particularly evident when the implementation of containers themselves obeys the coding standards of critical software, with no dynamic allocation and few pointers, as is the case for the bounded containers defined in the proposed Ada 2012 standard [3].

Standards for critical software development define comprehensive verification objectives to guarantee the high levels of dependability we expect of life-critical and mission-critical software. All requirements must be shown to be satisfied by the software, which is a costly activity. In particular, verification of low-level requirements is usually demonstrated by developing unit tests, from which high levels of confidence are only obtained at a high cost. This is the driving force for the adoption of formal verification on an equal footing with testing to satisfy verification objectives. The upcoming DO-178C avionics standard states: Formal methods [..] might be the primary source of evidence for the satisfaction of many of the objectives concerned with development and verification.

Although there are some areas where formal verification can be applied independently [START_REF] Souyris | Formal Verification of Avionics Software Products[END_REF], most areas where testing is the main source of evidence today would benefit from an integration of formal verification with existing testing practice. At the simplest, this combination should be provably sound and it should guarantee a coverage of atomic verifications through formal verification and testing. This is the goal of project Hi-Lite [14], a project aiming at combined unit testing and unit proof of C and Ada programs.

In the context of project Hi-Lite, this paper deals with the definition of suitable containers in Ada, based on Ada standard containers, whose properties can be both tested dynamically and proved automatically. Properties over containers offer a high level description of the code, suitable for expressing partial correctness in the form of code contracts. Therefore, we are not only interested in correct usage of container APIs, but also in partial correctness of functional properties of interest to users.

Before they can be used in the context of avionics (or similar) safety-critical software, the new library of formal containers will need to be certified and the verification tools we present will have to undergo qualification [START_REF]B: Software considerations in airborne systems and equipment certification[END_REF]. We present in this paper: (a) a formal proof of correctness of an implementation of the new library in Coq [START_REF]The Coq Proof Assistant[END_REF], a well-known formal programming language; and (b) a formal proof of the new library properties used in our verification tools, expressed in the Why language [START_REF] Filliâ T R E | The Why/Krakatoa/Caduceus Platform for Deductive Program Verification[END_REF] for formal verification. Thus, this work can be seen as a contribution to the argument-based approach to certification [START_REF] Rushby | Formalism in safety cases. In Chris Dale and Tom Anderson, editors, Making Systems Safer[END_REF].

In Section 2, we detail the changes that we introduce in formal containers w.r.t. containers as defined in language standards. In the following sections, we describe in detail formal containers for doubly linked lists, and we sketch formal containers for vectors, sets and maps: formal semantics in Section 3, formal specification in the Why language in Section 4, formal proof of correctness in Coq in Section 5. We finally give a survey of related works in Section 6.

A longer version of this article with more details and proofs is available on the web [4]. A web page gives an introduction to the code for containers' implementation and proofs [5], and instructions to anonymously access the git repository w h e r ea l lt h es o u r c ec od ei ss t o r e d .

Formal Containers

We will use the following Ada code as a running example throughout the section. Procedure Map_F1 modifies a list in place, by replacing each element initially contained in the list by its image through function F.

Contracts in Ada 2012

The forthcoming version of the Ada standard, called Ada 2012 [3], offers a variety of new features to express properties of programs. New checks are defined as aspects of program entities, for which the standard defines precisely the various points at which the check is performed during execution. The most prominent of these new checks are the Pre and Post aspects which define respectively the precondition and postcondition of a subprogram. These are defined as Boolean expressions over program variables and functions. For example, a simple contract on function Map_F could specify that its parameter list should not be empty, and that the call does not modify its length:

procedure Map_F (L : in out List) with Pre => Length (L) /= 0, Post => Length (L) = Length (L'Old);
Notice that, in the precondition, L refers to the list in the pre-state while, in the postcondition, L refers to the list in the post-state, hence the need to refer to the special attribute L'Old in the postcondition, which designates the value of L before the call. 2 The execution model for these aspects is simply to insert assertions at appropriate locations, which raise exceptions when violated. For each variable V whose pre-state value may be read in the postcondition (V'Old), the compiler inserts a shallow copy of the variable's value at the beginning of the subprogram body. It is this copy which is read to give the value of V'Old.

Expressing properties in contracts is greatly facilitated by the use of ifexpressions, case-expressions, quantified-expressions and expression-functions, all defined in Ada 2012. The main objective of these logic features is verification by testing, based on their executable semantics. In particular, quantifiedexpressions are always expressed over finite ranges or (obviously finite) containers, with a loop through the range or container as execution model: for all J in 0 .. 10 => P (J) is true if-and-only-if the subprogram P returns True for every argument, starting from 0 up to 10.

Ada Standard Containers

Like in many other languages, Ada standard containers define two mutually dependent data structures: containers proper which hold the data, and iterators (or cursors) which provide handles to individual pieces of data. In function Map_F, the container has type List and the iterator has type Cursor,whichare both defined by the standard Ada lists. A cursor is implicitly associated with a container (implemented as a pointer field in the cursor structure), in which it designates an element. An important feature of Ada containers is that cursors remain valid as long as the container exists and the element referenced is not deleted, like many iterators in other languages (for example those in C++ STL and Java JCL). This allows modifying a container while iterating over its content with cursors, without risk of invalidating these cursors.

API Modification: Independent Cursors

Problem. A useful postcondition for Map_F is to state how elements are modified by the call. All cursors are preserved through replacement of an element in a list. Thus, for every cursor Cu that designates an element E in L before the call, Cu designates F (E) in L after the call. It seems like we could express it with a quantified-expression:

procedure Map_F (L : in out List) with

Post => (for all Cu in L => Element (Cu) = ???);

The expression denoted by ??? should designate the value obtained by calling F (Element (Cu)) in the pre-state, which could be intuitively written as F (Element (Cu))'Old. Unfortunately, this expression is not valid because it refers to the value in the pre-state of Cu, which is not defined in the pre-state since it is quantified. As a side note, notice that, even for a cursor Cu defined outside of the Map_F function, Cu'Old would be the same as Cu in our example, because the semantics of attribute 'Old is to perform a shallow copy, so it does not copy the implicit container in a cursor. Approach. To solve the previous two problems, we break the implicit link between cursors and containers, so that the same cursor can be used both in the pre-state and in the post-state. Then, the previous postcondition can be expressed easily:

procedure Map_F (L : in out List) with Post => ( for all Cu in L= > Element (L, Cu) = F (Element (L'Old, Cu)));
Notice that we passed an additional argument to function Element,t oi ndicate the container from which the element at cursor Cu should be retrieved. This is true for every function in the API of containers which previously accessed implicitly the container through a cursor, such as Next in the example of Section 2. This is the only modification to the API of containers that we introduce. The alternative of using existing containers both greatly complicates the execution model and the formal verification.

Using existing containers would require a different semantics for the 'Old attribute, which would reach to the complete pre-state including the stack and heap, similar to the work by Kosiuczenko on Java programs [START_REF] Kosiuczenko | An abstract machine for the old value retrieval[END_REF] that builds a complete history of updates alongside execution. Our solution has the benefits of sticking to the standard semantics for 'Old in Ada 2012, leading to a simple and efficient execution model.

The semantics of standard cursors also leads to more complex verification conditions to check the correct use of containers' API: each access through cursor Cu to container Co is valid only if 1) Co is alive, which can be hard to know if Co is implicit, and 2) Cu is associated to container Co, which amounts to deciding whether Co is the same as the implicit container in Cu. With the semantics of formal containers, both verification conditions above disappear.

API Addition: Parts of Containers

Problem. In order to prove the postcondition of Map_F stated above, we need to annotate the loop in Map_F with a loop invariant, which states the accumulated effect of N iterations through the loop. We would like to state that list elements already scanned have been modified by F (as in the postcondition) and that list elements not yet scanned are unchanged. This pattern of loop invariant, consisting of two parts for the elements scanned and the elements not yet scanned, is typical of loops that iterate over a container.

Approach. We introduce two new functions, called Left and Right,w h i c h return the containers holding respectively the elements preceding (exclusively) or following (inclusively) a given cursor in the container. With these functions, the effect of the loop on the elements already scanned resembles the postcondition:

pragma Assert ( for all Cu in Left (L, Current) => Element (L, Cu) = F (Element (L'Old, Cu)));
The effect of the loop on the elements not yet scanned is not simply the equality of right containers. Indeed, equality of lists L1 and L2 only implies that, while iterating separately through each of the lists, the same elements are encountered in the same order. Here, we also need to be able to iterate on both lists with the same cursor, so that the first cursors of L1 and L2 should be equal and then each call to Next should return the same cursor on both lists which is not implied by equality. This is expressed with a new function, called Strict_Equal:

pragma Assert (Strict_Equal (Right (L, Current), Right (L'Old, Current)));
3F o r m a l S e m a n t i c s

In this section, we present a formal semantics for lists. We show briefly how the formal semantics of other containers compares to the one of lists in the last subsection.

Syntax of Lists

A program is a sequence of variable declarations for lists (in Lvar)a n dc u rsors (in Cvar) followed by a sequence of instructions (in Instr). Procedures Insert, Delete and Replace Element modify their first argument, which must be therefore a variable, and have no return value. The remaining instructions are assignments. Notice that list assignment makes an explicit copy of its argument, which prevents aliasing between lists. LExpr is the set of list expressions. For the sake of simplicity, we only list instructions and expressions that are specific to containers. Thus, we have not included loops or branching statements in the set of instructions, or arithmetic operations in the set of integer expressions.

Operational Semantics of Lists

Since lists are generic in the kind of element they contain, the type E of elements is left unspecified. The type D of cursors can be any countably infinite type. We add a specific element ⊥ to this set, D∪⊥ is written D ⊥ . There is an environment for lists Γ L , and an environment for cursors Γ C :

Γ L : Lvar → L = {Len : N, Fc :[1..Len ] ֒→ D, Fe : Im(Fc) → E} Γ C : Cvar → D ⊥
Intuitively, lists can be seen as an array Fc of cursors with a mapping Fe from cursors to elements. Fc is injective, so Fc restricted to Im(Fc) is bijective, and Fc -1 : Im(Fc) → [1..Len ] is its inverse. We extend Fc -1 to Fc -1

+ : Im(Fc) ∪ {⊥} → [1..Len +1] with Fc -1 + (⊥)=Len + 1.
Given an instruction I in Instr, a list l in LExpr,ac u r s o rc in CExpr, an expression e in EExpr,aB o o l e a n expression b in BExpr and an integer expression i in IExpr, judgments take the following form: ,c) is defined only when d ∈ Im(Fc), which is expressed in the informal semantics as c designates an element in l. Indeed, the associated Ada function will raise a run-time error otherwise. Has Element (l, c)checksifc effectively designates an element in l. Equality over lists (=) is the structural equality. It only implies that the elements in its two list arguments appear in the same order, i.e., the equality of Fe • Fc :[1..Len ] → E. Strict Equal is stronger than =, as expected, since it also implies the equality of Fc and Fe . Equality of cursors is simply equality of their evaluations.

Γ L ,Γ C ⊢ I ⇒ Γ ′ L ,Γ ′ C Γ L ,Γ C ⊢ l ⇒ L Γ L ,Γ C ⊢ c ⇒ D ⊥ Γ L ,Γ C ⊢ e ⇒ E Γ L ,Γ C ⊢ b ⇒ B Γ L ,Γ C ⊢ i ⇒ Z If expr is an expression, Γ L ,Γ C ⊢
ΓL,ΓC ⊢ l ⇒{Len , Fc, Fe } ΓL,ΓC ⊢ Length (l) ⇒ Len ΓL,ΓC ⊢ l ⇒{Len , Fc, Fe } ΓL,ΓC ⊢ c ⇒ dd ∈ Im(Fc) ΓL,ΓC ⊢ Element(l, c) ⇒ Fe (d) ΓL,ΓC ⊢ l ⇒{Len , Fc, Fe } ΓL,ΓC ⊢ c ⇒ d ΓL,ΓC ⊢ Has Element (l, c) ⇒ d ∈ Im(Fc) ΓL,ΓC ⊢ l1 ⇒{Len 1, Fc1, Fe 1} ΓL,ΓC ⊢ l2 ⇒{Len 2, Fc2, Fe 2} ΓL,ΓC ⊢ l1 = l2 ⇒ Len 1 = Len 2 & Fe 1 • Fc1 = Fe 2 • Fc2 ΓL,ΓC ⊢ l1 ⇒{Len 1, Fc1, Fe 1} ΓL,ΓC ⊢ l2 ⇒{Len 2, Fc2, Fe 2} ΓL,ΓC ⊢ Strict Equal (l1,l2) ⇒ Len 1 = Len 2 & Fc1 = Fc2 & Fe 1 = Fe 2 ΓL,ΓC ⊢ c1 ⇒ d1 ΓL,ΓC ⊢ c2 ⇒ d2 ΓL,ΓC ⊢ c1 = c2 ⇒ d1 = d2
Below are the description of the semantics of cursor expressions.

ΓL,ΓC ⊢ No Element ⇒⊥ ΓL,ΓC ⊢ l ⇒{Len , Fc, Fe } ΓL,ΓC ⊢ c ⇒ d1 d1 ∈ Im(Fc) ∪{⊥} ΓL,ΓC ⊢ Next (l, c) ⇒ d2 where d2 = {Len =0 & d1 ∈ Im(Fc)\{Fc(Len )}→Fc(Fc -1 (d1)+1), else →⊥} ΓL,ΓC ⊢ l ⇒{Len , Fc, Fe } ΓL,ΓC ⊢ c ⇒ d1 d1 ∈ Im(Fc) ∪{⊥} ΓL,ΓC ⊢ Previous(l, c) ⇒ d2 where d2 = {Len =0 & d1 ∈ Im(Fc)\{Fc(1)}→Fc(Fc -1 (d1) -1), else →⊥} ΓL,ΓC ⊢ l ⇒{Len , Fc, Fe } ΓL,ΓC ⊢ First (l) ⇒ d where d = {Len =0→⊥, Len > 0 → Fc(1)} ΓL,ΓC ⊢ l ⇒{Len , Fc, Fe } ΓL,ΓC ⊢ Last (l) ⇒ d where d = {Len =0→⊥, Len > 0 → Fc(Len )}
Below are the description of the semantics of list expressions. The empty list, returned by Empty, is the only list whose length is null (F ∅ is the only function that is defined on the empty set ∅). Left is defined for both valid cursors and No Element . Its evaluation yields a list whose valid cursors are the valid cursors of the list argument which precede cursor argument c (when c is No Element , that means all cursors). Right is similar.

ΓL,ΓC ⊢ Empty ⇒{0, F∅ , F∅ } ΓL,ΓC ⊢ l ⇒{Len , Fc, Fe } ΓL,ΓC ⊢ c ⇒ dd ∈ Im(Fc) ∪{⊥} n = Fc -1 + (d) -1 ΓL,ΓC ⊢ Left (l, c) ⇒{ n, Fc ′ , Fe ′ } where Fc ′ = Fc| [1..n] Fe ′ = Fe | Im(Fc ′ ) ΓL,ΓC ⊢ l ⇒{Len , Fc, Fe } ΓL,ΓC ⊢ c ⇒ dd ∈ Im(Fc) ∪{⊥} n = Fc -1 + (d) -1 ΓL,ΓC ⊢ Right (l, c) ⇒{Len -n, Fc ′ , Fe ′ } where Fc ′ = λi :[1..Len -n].Fc(n + i) Fe ′ = Fe | Im(Fc ′ )
The rules below describe the semantics of instructions. Rules concerning reads or assignment of variables are omitted (they are the usual ones). Insert modifies the environment so that its list variable argument designates, after the call, a list where a cursor and an element have been inserted at the proper place. The cursor argument, which can be either a valid cursor or No Element , encodes the place the new element is inserted. The newly created cursor is not specified. It should be different from No Element and from every valid cursor in the argument list.

Delete modifies the environment so that its cursor variable argument (which must reference a valid cursor before the call) is deleted from the list referenced by its list variable argument. The cursor variable references the special invalid cursor No Element after the call. Replace Element modifies the environment so that, after the call, its cursor argument (which must be valid) designates its element argument in the list referenced by its list variable argument.

ΓL(l)={Len , Fc, Fe } ΓL,ΓC ⊢ c ⇒ d1 d1 ∈ Im(Fc) ∪{⊥} n = Fc -1 + (d1) d2 / ∈ Im(Fc) ∪{⊥} ΓL,ΓC ⊢ e ⇒ Elt ΓL,ΓC ⊢ Insert (l, c, e) ⇒ ΓL[l →{Len +1, Fc ′ , Fe ′ }],ΓC where Fc ′ = λi :[1..Len +1]. {i ∈ [1..n -1] → Fc(i),i = n → d2,i ∈ [n +1..Len +1]→ Fc(i -1)} Fe ′ = λd : Im(Fc ′ ).{d ∈ Im(Fc) → Fe (d),d = d2 → Elt} ΓL(l)={Len , Fc, Fe } ΓC (c)=dd ∈ Im(Fc) n = Fc -1 (d) ΓL,ΓC ⊢ Delete(l, c) ⇒ ΓL[l →{Len -1, Fc ′ , Fe ′ }],ΓC[c →⊥] where Fc ′ = λi :[1..Len -1].{i ∈ [1..n -1] → Fc(i),i ∈ [n..Len -1] → Fc(i +1)} Fe ′ = Fe | Im(Fc ′ ) ΓL(l)={Len , Fc, Fe } ΓL,ΓC ⊢ c ⇒ d1 d1 ∈ Im(Fc) ΓL,ΓC ⊢ e ⇒ Elt ΓL,ΓC ⊢ Replace Element (l, c, e) ⇒ ΓL[l →{ Len , Fc, Fe ′ }],ΓC
where Fe ′ = λd : Im(Fc).{d = d1 → Elt,d = d1 → Fe (d)}

Vectors, Sets and Maps

Sets. Sets do not allow duplication of elements, the order of iteration in a set is not user-defined and the link between cursors and elements is preserved in most cases. In the semantics, sets can be modeled as the same tuples as lists where Fe is injective: {Len : N, Fc :[1.

.Len ] ֒→ D, Fe : Im(Fc) ֒→ E}. For non ordered sets, the order of iteration is not specified. If the set is ordered, the order of iteration is constrained by the order over elements. As a consequence, function Fe • Fc has to preserve order. The longer version of this article presents the modified inference rule for Insert for each container.

Maps. Maps behave just like sets of pairs key/element except that they only constrain keys:

(k 1 ,e 1 ) < (k 2 ,e 2 ) ↔ k 1 <k 2 and (k 1 ,e 1 )=(k 2 ,e 2 ) ↔ k 1 = k 2 .
Ve cto rs . Vectors do not expect cursors to keep designating the same element in every case. Instead, as for arrays, elements can be accessed through their position (an index). As a consequence, we model vectors as tuples {Len : N, Fc : [1.

.Len ] ֒→ D, Fe :[ 1 ..Len ] → E} where Fc is injective. When an element is inserted or deleted from a vector, nothing can be said for the cursors that follow the place of insertion/deletion.

Axiomatization

In this section, we present an axiomatization of lists in the language Why, targeted at automatic provers. We show that this axiomatization is correct w.r.t. the formal semantics we gave in Section 3. We will formally prove it is correct w.r.t. formal semantics in Coq in Section 5.

Presentation of Why

The Why platform [START_REF] Filliâ T R E | The Why/Krakatoa/Caduceus Platform for Deductive Program Verification[END_REF] is a set of tools for deductive program verification. The first feature of Why is to provide a common frontend to a wide set of automated and interactive theorem provers. Why implements a total, polymorphic, firstorder logic, in which the user can declare types, symbols, axioms and goals. These goals are then translated to the native input languages of the various supported provers. In our case, we are using the backends for the Coq proof assistant [START_REF]The Coq Proof Assistant[END_REF] and the three SMT solvers Alt-Ergo [START_REF] Conchon | The Alt-Ergo automatic theorem prover[END_REF], Z3 [START_REF] De Moura | Z3, An Efficient SMT Solver[END_REF] and Simplify [START_REF] Detlefs | Simplify: a theorem prover for program checking[END_REF].

For example, here is some Why syntax that declares a modulo operation over integers, together with some possible axiomatization: The second feature of Why we use here is to provide a verification condition generator for an idealized, alias-free, Hoare-logic-like programming language. The user declares and implements programs, which are annotated with preand postconditions, and local assertions such as loop invariants. Verification conditions are then generated and transmitted to the theorem provers. Here is for instance the declaration of a program function W h e nu s e d inside programs, this function will trigger verification conditions (namely, that its second argument is positive). This is one way to express that modulo is a partial operation.

Axiomatization of Lists

Note that this axiomatic is not meant to be the exact translation of our semantics, but rather is written to facilitate the verification of programs with automatic provers.

Types. The type of elements is irrelevant, and so it is defined as an abstract type element_t. Cursors and lists are described respectively with abstract types cursor and list, further axiomatized in the following.

Properties. To encode the semantics defined in Section 3, we introduce three logic functions:

logic length_ : list -> int logic position_ : list , cursor -> int logic element_ : list , cursor -> element_t Logic functions length_ and element_ define accessors to the fields Len and Fe of a list. The encoding is more complex for the field Fc, due to the fact that Fc is used in three different ways in the specification: 1) directly, 2) through its inverse Fc -1 , and 3) through its domain Im(Fc). Function position_ is the extension of Fc -1 to cursors not in Im(Fc), whose image is set to 0. It gives access to both Im(Fc)( c ∈ Im(Fc) ⇔ position_(l, c) > 0)a n d Fc -1 . We rewrite almost all rules of the semantics to remove occurrences of Fc. For example, in the rule for Next, d 2 = Fc(Fc -1 (d 1 ) + 1) can be rewritten as Fc -1 (d 2 )=Fc -1 (d 1 ) + 1. The only rule that cannot be translated that way is =. For this one rule, we can use an existential quantification,

∀ d 1 : Im(Fc 1 ).∃ d 2 : Im(Fc 2 ).Fc -1 1 (d 1 )=Fc -1 2 (d 2 )&Fe 1 (d 1 )=Fe 2 (d 2 )
. Why functions length_, element_ and position_ are related to the semantics as follows:

∀ l, i, length_(l) = i ⇔∃ Len , Fc, Fe , ΓL,ΓC ⊢ l ⇒{ Len , Fc, Fe } & Len = i ∀ l, c, i, position_(l, c) = i ⇔∃ Len , Fc, Fe ,d , ΓL,ΓC ⊢ l ⇒{ Len , Fc, Fe } & ΓL,ΓC ⊢ c ⇒ d & i ≥ 0&( i =0→ d/ ∈ Im(Fc)) &( i > 0 → d ∈ Im(Fc)&Fc -1 (d)=i) ∀ l, c, e, position_(l, c) > 0 → element_(l, c) = e ⇔∃ Len , Fc, Fe ,d ,Elt, ΓL,ΓC ⊢ l ⇒{ Len , Fc, Fe } & ΓL,ΓC ⊢ c ⇒ d & ΓL,ΓC ⊢ e ⇒ Elt &( d ∈ Im(Fc) → Fe (d)=Elt)
Axioms. We encode the semantic properties of functions length_ and position_ into axioms, while ensuring that the axiomatic is not unnecessarily restrictive (all semantic lists should be also axiomatic lists). We have four axioms:

1. ∀ l, length_(l) >= 0 2. ∀ l, c, length_(l) >= position_(l, c) >= 0 3. ∀ l, position_(l, no_element) = 0 4. ∀ l, c1, c2, position_(l,c1) = position_(l,c2) > 0 → c 1=c 2
It is rather straightforward to check that these axioms are implied by the semantics. These proofs can be found in the longer version of this article. The precondition of this function states that either the argument cursor c is valid in the argument list l (because position_(l, c) > 0 ⇔ c ∈ Im(Fc)) or the argument cursor is equal to No Element . This precondition is exactly the condition for the application of the semantic rule for Next.

An axiom next__ defines the behavior of logic function next_ over the allowed cases only, leaving the value of other applications of next_ unspecified, as seen in Section 4.1: Axiom next__ is defined as two implications: in the first case, the next cursor of the cursor argument is valid and we define its position; in the second case, the result is No Element. Intuitively, this is the same as the semantic rule for Next. Using the same equivalences as above, we can rewrite axiom next__ i n t oal o g i c formula that is exactly the semantics of Next, rewritten to use only Fc -1 .T h i s proof is presented in the longer version of this article.

Effectiveness

It is worth noting that the main difficulty we faced, when developing the axiomatization presented above, was to match the somewhat fuzzy expectations of SMT automatic provers: some work best with large predicates and few axioms, some work best with many smaller axioms, etc.

We wrote a number of tests (30) to convince ourselves that the axiomatization of lists presented is effective. With a combination of provers we managed to prove all the generated verification conditions. Our running example is proved rather quickly (less than 1s per VC). To facilitate proofs, which impacts both provability and speed, we defined 15 lemmas. These are not a burden in the maintainability of the axiomatic and cannot introduce inconsistencies since they are also automatically proved.

Most of the tests correspond to unit-tests for specific properties of list expressions (especially for complex ones, such as Left ) and instructions. For example, there is a test to check that after replacing the value of an element in the list, the list indeed contains this value at this position after the call:

Validation of the Axiomatization

We have presented a formal semantics for containers in Section 3 and its axiomatization in Why in Section 4. We have shown a pen-and-paper proof that the axiomatization presented is correct w.r.t. formal semantics. Given the size of the axiomatization, such a manual proof may easily contain errors. In this section, we describe an implementation in Coq of the formal semantics of containers, and a formal proof of correctness of the Why axiomatization of lists w.r.t. the Coq implementation, (which also implies the consistency of the axiomatization).

Coq Implementation and Proof for Lists

Types. Our proofs are generic in the element type. For the representation of cursors, we use positive natural numbers to which we add 0 to model the special cursor ⊥. For lists, we model the tuple with a functional list of pairs cursorelement (if a is an element of this list, fst a refers to the associated cursor and snd a to the element). The field Len is the length of the functional list, the field Fc is the function that, for an integer i ∈ [1.

.Len ], returns the cursor of the pair at the i th position in the list and Fe returns, for each cursor in Im(Fc), its first association in the list. Therefore, a list of this kind always defines one and only one tuple {Len , Fc, Fe }.

Definition cursor : Set := nat. Definition Rlist : Set := List.list (cursor*element_t ).

To keep only tuples where Fc is injective and has value in D,w ec o n s t r a i nt h e functional lists with a predicate. This predicate states that every cursor that appears in a list is different from ⊥ (positive) and does not appear again in the same list. Axioms. Thanks to the -coq option of Why, we translate automatically our Why axioms into Coq. They can then be proved valid formally.

Semantic Rules. We have written an implementation for each construct of our language. Since Coq is a pure functional language, the instructions that modify their list argument, such as Insert , are modeled by a function that returns a new list. The implementations are as close as possible to the semantic of their corresponding construct. Since they are Coq functions, these implementations have to be total, so we complete them for the cases that are not described in the semantics. For example, the semantics of Next is only defined when the cursor that designates the element to be replaced is valid in the list or equal to No Element3 . In the Coq implementation below, it returns No Element if we are not in that case (we could have chosen any other return value). The result of the semantic rule for Next is completely defined. It is easy to be convinced that, when the cursor given as a parameter is indeed valid in the list or equal to No Element , the Coq function next returns the appropriate cursor. We use this representation to prove formally that the contracts in our axiomatic are indeed implied by the semantics.

For nearly every rule of the semantics of lists, the result of the modification is completely defined in terms of the value of the arguments. The only rule that is not completely determined is Insert , since the value of the new cursor is not given. For the implementation, we define a function new that returns a valid cursor. To keep our proofs as general as possible, we took care to use only the properties of new that were defined in the semantic (i.e., that the result of new / ∈ Im(Fc) ∪⊥) by enforcing it thanks to Coq's module system.

Vectors, Sets and Maps

All containers have the same Coq representation. Therefore, some parts of the proofs are shared. Sets and maps (ordered or not) share the same lemmas and heavily rely on those of lists. Vectors also rely on the lemmas of lists but less heavily (they are quite different). To make the proofs more reliable, general lemmas, which will not be affected by a slight change in the API, are collected in a separate file named "Raw". Here are the size of the files (the number of lemmas in each file) and the architecture. Like for the Insert rule for lists, every unspecified part of the semantic of every container is kept as general as possible thanks to a sealed Coq module that only allows proofs to use the specified parts. The whole proof is 16,000+ lines of Coq. All of it plus commented excerpts can be found on the web.

Related Work

Formal proof over containers is an active area of research. There are two important, complementary areas in this domain: certifying user code that uses containers while assuming that their implementation complies with their specification (what we are doing) and certifying that an implementation of containers indeed complies with its specifications. On the one hand, Bouillaguet et al. focus on verifying that a container's implementation indeed complies with its specifications. They use resolution based first-order theorem provers to verify that the invariants of data structures such as sets and maps are preserved when considering operations on their encodings as arrays and trees. Zee et al. [START_REF] Zee | Full functional verification of linked data structures[END_REF] even presented the first verification of full functional correctness for some linked data structure implementations. Unlike Bouillaget et al., they use interactive theorem provers as well to discharge their verification conditions. Since they aim at certifying an implementation once, it does not seem to be too heavy a burden.

On the other hand, Gregor and Schupp [START_REF] Gregor | STLlint: lifting static checking from languages to libraries[END_REF] focus, like we do, on the certification of user programs. They present an unsound static analysis of C++ programs using STL containers. They generate partially executable assertions in C++ to express the constraints over containers' usage, in particular a nonexecutable foreach quantifier to iterate over all objects of a given type in the current memory state. Blanc et al. [START_REF] Blanc | Verifying C++ with STL containers via predicate abstraction[END_REF] also work on certifying user code using the C++ STL containers. Just as we did in this work, they axiomatize the containers and then construct some preconditions (resp. postconditions) that are more (resp. less) constraining than those of the semantics. Their work is still substantially different from what we did since they only check that the containers are properly used and they have no annotation language to allow the user express other properties. Dillig et al. [START_REF] Dillig | Precise reasoning for programs using containers[END_REF] present a static analysis for reasoning precisely over the content of containers. While they assume that we can analyze the code that fills the containers to provide constraints over the containers' content, we rely instead on user annotations. This gives us the possibility to verify user properties expressed in the same annotation language.

7C o n c l u s i o n

We have presented a library of formal containers, a slightly modified version of the standard Ada containers. The aim was to make them usable in programs annotated with properties of interest to the user, that can be both tested and formally proved automatically. Although we have limited experience with using this library, our experiments so far indicate that most user-defined annotations can now be expressed with few quantifiers, leading to automatic proofs of rich properties with SMT provers. We are now looking forward to working with our industrial partners in project Hi-Lite to develop large use-cases with formal containers.

We have given a formal semantics for these containers, and we have proved that this semantics is consistent by implementing it in Coq. We have developed an axiomatization of these containers in the language Why, targeted at automatic proofs with SMT provers, and we have proved in Coq that this axiomatization is correct w.r.t. the formal semantics of containers. On the one hand, this formalization is an essential step towards an argument-based certification of the library of formal containers, for their use in safety-critical software development. On the other hand, the proof of correctness of the axiomatization used in automatic provers is a very strong assurance against inconsistencies in proofs, which are a sour point of formal methods in industry.

Formal containers have been implemented in Ada, and could be included in any Ada compiler's library. They have been included in the standard library of the not yet released GNAT 6.5 Ada compiler. Theoretically, the Why axiomatization could be reused to model containers in other languages, with a few modifications to comply with the particularities of their respective APIs. The implementation we provide for Ada containers should be correct w.r.t. the formal semantics in Coq, but we have not proved it formally. This is an interesting (but difficult) problem for the future.

M

  . Gogolla and B. Wolff (Eds.): TAP 2011, LNCS 6706, pp. 102-118, 2011. c Springer-Verlag Berlin Heidelberg 2011

  Instr := Insert(LVar, CExpr, EExpr) | Delete(LVar, CVar) | Replace Element (LVar, CExpr, EExpr) | Cvar := CExpr | Lvar := Copy(LExpr) | ... LExpr := Lvar | Empty | Left (LExpr, CExpr) | Right (LExpr, CExpr) IExpr := Length (LExpr) | ... CExpr := Cvar | No Element | First (LExpr) | Last (LExpr) | Next (LExpr, CExpr) | Previous (LExpr, CExpr) EExpr := Element (LExpr, CExpr) | ... BExpr := Has Element(LExpr, CExpr) | LExpr = LExpr | CExpr = CExpr | Strict Equal (LExpr, LExpr) | ...

  logic mod_ : int, int -> int axiom mod__ : forall a, b : int. 0 < b -> exists q:i n t .a=b*q+mod_(a, b) and 0 <= mod_(a, b) < b goal test : mod_(7, 2) = 1

  parameter mod : a : int -> b : int -> {0 < b} int {result = mod_(a, b)} which takes two integers a and b as arguments, has precondition 0<b , returns ar e s u l to ft y p eint and has postcondition result = mod_(a, b).

  Semantic Rules. Each Ada function represented in the semantics is translated into a Why program. Given the semantic rule Pre S Post S defining this function, we define a precondition Pre A and a postcondition Post A on the Why program, so that Pre A ⇒ Pre S and Post S ⇒ Post A . In fact, since preconditions are quite simple, we usually have Pre A = Pre S . We illustrate the general pattern that we applied with function Next, which we translate into program next in Why: parameter next : l:list -> c:cursor -> { c = no_element or position_(l, c) > 0 } cursor { result = next_(l, c) }

  axiom next__ : forall l:list. forall c:cursor. forall nxt:cursor. (length_(l) > position_(l,c) > 0 -> position_(l, nxt) = position_(l, c) + 1) and (length_(l) > 0 and position_(l, c) = length_(l) or c = no_element -> nxt = no_element )

Fixpoint

  well_formed (l : Rlist) : Prop := match l with nil => True | a :: ls => fst a > 0 /\ has_element ls (fst a) = false /\ well_formed (ls) end. Record list := {this :> Rlist; wf : well_formed this}.The property of well formedness has to be preserved through every modification of the list. With the Coq lists restricted that way, there is one and only one list per tuple {Len : N, Fc :[ 1 ..Len ] ֒→ D, Fe : Im(Fc) → E}. The two representations are equivalent.

Fixpoint

  next (l : Rlist) (cu : cursor) := match l with nil => no_element | a :: ls => if beq_nat (fst a) cu then first ls else next ls cu end.

  Empty is the empty list constant. Functions Left and Right return parts of containers as defined in Section 2.4. CExpr is the set of cursor expressions. No Element is the constant invalid cursor. Functions First , Last , Next and Previous are used for iterating over lists. EExpr is the set of element expressions. Function Element accesses the element designated by a cursor in a list. BExpr is the set of Boolean expressions. Has Element checks for the validity of a cursor in a given container, = is the structural equality and Strict Equal is the more constraining equality described in Section 2.4. Finally, IExpr is the set of integer expressions. Function Length returns the length of a list.

  expr ⇒ val means that expr evaluates in environments Γ L and Γ C to a value represented by val in the semantics. If instr is an instruction, Γ L ,Γ C ⊢ instr ⇒ Γ ′ L ,Γ ′ C means that instr change the environments Γ L and Γ C into Γ ′ L and Γ ′ C . Below are the description of the semantics of integer, element and boolean expressions. The result of function Length on a list evaluating to {Len , Fc, Fe } is Len . Similarly, function Element returns the value of Fe on d, where cursor argument c evaluates to d.N o t i c et h a tElement (l

  Therefore ⊥ is not a valid cursor, i.e., it designates no element, in any list. Function Next is defined for both valid cursors and No Element . It returns No Element when applied to a cursor which has no valid successor (i.e., for No Element and the last cursor). Previous is similar. Function First is defined on every list. It returns No Element when called on an empty list. Last is similar.

The special invalid cursor No Element evaluates to ⊥. This is possible because ⊥ cannot appear in Im(Fc), as Fc :[1..Len ] → D.

  Vectors, Sets and MapsHere is a table referencing the work done for each container. It contains the size of its Why file (its number of lines), the number of lemmas given and the number of tests passed. The code and tests are available on the web.

	let test_replace_element
	(co : list ref) (cu : cursor) (e : element_t) =
	{ has_element_ (co, cu) }
	replace_element co cu e
	{ element_ (co, cu) = e }
	A few tests, such as our running example, combine expressions and instructions
	to validate more complex behaviors of the API. All tests were proved automat-
	ically.
	4.4 Container	Lines Lemmas Tests	Container	Lines Lemmas Tests
	List	352	15	30	Ordered Sets	506	30	38
	Vectors	298	0	22	Hashed Maps	394	27	22
	Hashed Sets 429	24	35	Ordered Maps 476	35	25

Note that Map F is client code, not part of the API.

More precisely, attribute 'Old can be applied to all names (as defined in Ada standard), so that we could use Length (L)'Old instead of Length (L'Old).

Using it elsewhere reflects a mistake and is reported as an error when executed.

Acknowledgement. We would like to thank Ed Schonberg, David Lesens and the anonymous referees for their useful reviews of this paper.