LCPC François De Larrard

John Chandler
email: jchandler@trl.co.uk

Jorgen Christensen

Ferhat Hammoum
email: hammoum@lcpc.fr

Anders Henrichsen

Tatiana Himerik

Nina Sliwa
email: sliwa@bast.de

Jussara Tanesi

Finn Thoegersen

George Vorobieff
email: george_vorobieff@rta.nsw.gov.au

A Cementitious Long-Life Wearing Course to Reduce Frequency of Maintenance Works on High-Traffic Roads

come

Introduction

Under the framework of OECD (Organisation for Economic Cooperation and Development), ECMT (European Conference of Ministers of Transport) and their Joint Transport Research Centre (JTRC), a number of road laboratories have worked together to develop the concept of a long-life wearing course for highly trafficked pavements. The first phase of the JTRC-IM3 project indicated through an economic analysis, that, for some specific applications, it was worth studying technical solutions that could extend the service life for up to 20, 30 or 40 years, with no maintenance nor traffic disruption during this period [START_REF]Economical evaluation of long-life pavements[END_REF]. In Phase II of the project, two technical families were evaluated; a bituminous and a cementitious surfacing. The innovative High-Performance Cementitious Material (HPCM) solution consists of applying an 8-mm layer of ultra-high performance, fibre reinforced fine mortar, in which hard, polish-resistant aggregate particles are embedded [START_REF] De | Preliminary tests on a hydraulic surface dressing for wearing courses with a long life[END_REF][START_REF] De | A high-performance cementitious surface dressing for long-life wearing courses[END_REF][START_REF] Oecd/Ecmt | Long-Life Surfaces for Busy Roads -Economical evaluation of long-life pavements. Phase II[END_REF]. The paper gives the results of the HPCM material development. In conclusion, the perspectives opened by this new technology are briefly presented.

Design of the HPCM complex

One of the most important requirements of a wearing course is the need for good skid resistance, which is dependent upon the aggregate in the surfacing. For a long-life top layer, it is thus necessary to choose an aggregate with a superior polishing resistance. According to general experience, calcined bauxite, an artificial aggregate obtained by subjecting a natural mineral to a thermal treatment, is recognised as one of the best solutions. However, it is an expensive material, with limited suppliers: its unit cost may range from 30 to 40 times that of ordinary aggregates. Therefore, a surface dressing which only comprises a single layer of particles is relevant. Among available aggregate fractions, the 3-7 mm size has been chosen, because a maximum size of aggregate of around 6 mm tends to be the optimum size when a combination of adequate skid resistance and limited noise emission is required.

The next requirement is the design of the binder, the key function of which is to stick the calcined bauxite chippings to the pavement. When the option of using a hydraulic binder is taken, one must develop a fine material with the maximum tensile strength obtainable on site. From the experience gained with the ultra-high performance concretes [START_REF] De | Optimization of Ultra-High Performance Concrete by Using a Packing Model[END_REF][START_REF] Richard | Les bétons de poudres réactives (BPR) à ultra-haute résistance (200 à 800 MPa)[END_REF], a design mix of sand, Portland cement, silica fume, superplasticizer and water, with a low water/binder ratio is suitable. As in the ultra-thin white topping technology [START_REF] Rasmussen R | Thin and Ultra-Thin Whitetopping -A Synthesis of Highway Practice[END_REF], a good bond is expected between the cementitious mortar and the bituminous substrate. However, due to the shrinkage of the mortar which will be restrained by the pavement structure, cracking is likely to occur. To limit the crack opening, some sort of reinforcement is needed, but, given the thinness of the mortar layer, only fibres added to the mix are appropriate. The thickness of this fibre-reinforced mortar should be minimal for economic reasons. However, it should prevent the chippings from coming into direct contact with the asphalt layer. Moreover, the chippings/mortar composite should form a strong protecting layer for the lower pavement layers. Thus a thickness of 8 mm is selected for the mortar.

The following constituents were taken for the original mixture designs, based on previous experience of the participating laboratories:

• a 3/7 mm calcined bauxite from China • an aeolian siliceous fine sand • a Portland cement CEM I • a light grey silica fume from Norway • a polycarboxylate-type superplasticizer in powder form • steel fibres with a length of 13 mm and a diameter of 0.2 mm • alternatively, PVA (polyvinyl alcohol) fibres with a length of 15 mm and a diameter of 0.33 mm.

As for the mixture proportions, three ratios were fixed arbitrarily: the water/cement ratio (0.2), the silica-fume/cement ratio (0.2) and the dry superplasticizer/cement ratio (0.003), based on previous experience. As for the fibrous reinforcement, both the type and dosage rate of the fibres had to be determined later, after the results of some specific tests.

A first mortar recipe was developed and tested among the different participants. Later, it was adjusted in order to get a more stable rheological behavior at the fresh state and a better bond, thanks to a softer consistency. Table 1 displays the optimised recipe used in most of the tests performed during the project. This mortar had to incorporate fibres in order to resist to the shrinkage-induced tensile stresses.

Plain mortar tests

Table 2 displays the main mechanical properties of the mortar, with 4% PVA fibres. The shrinkage of plain mortar was measured on 7x7x28 cm specimens, from 1 day up to 250 days. The final autogenous shrinkage was about 650 microstrains, and total shrinkage at 50 % R.H. attained a value of 800 microstrains. Also, the coefficient of thermal expansion was found to be equal to 17.6x10 -6 . Therefore, it was verified that this material has the ability to crack in restrained conditions, whatever the outer humidity; fibres are definitely required if cracking is to be avoided. The fiber reinforced mortar was also subjected to up to 25-million of flexural fatigue cycles. With at least 2 % of fibres, it was found that the material could resist, only showing a decrease and a stabilisation of the apparent E-modulus, whatever the nature of the fibres.

Cracking tests

The cracking tests were decisive in selecting the type and dosage of fibres. Two campaigns of insitu cracking tests were carried out, where 6-m long, 14-cm wide strips were laid in parallel on an old asphalt pavement (see Fig. 1). After some months, it was tentatively concluded that either 3 % of steel fibres or 4 % of PVA fibres could equally well prevent cracking. The latter solution was preferred, owing to better workability and lower cost induced by these synthetic fibres. A large, 20x2 m test pad was cast, in order to check that no cracking would appear at full scale. Unfortunately, after a hot early summer, it was found that PVA fibres tended to soften; this reinforcement was then no longer able to overcome the crack development in the strips, unlike steel fibres. Consequently, the final solution recommended by the authors is to use at least 3% of steel fibres to eliminate any visible cracking. This finding is also confirmed by a series of laboratory cracking tests performed on the mortar phase.

Surface resistance tests

Various tests were applied on laboratory specimens, in order to investigate the likelihood of surface distress under traffic. Rutting testers, with a cornering angle, resulted in a chipping loss of about 7.5 % in a HPCM specimen, a value that can be compared to 4.5 % obtained with a typical epoxy-asphalt surface dressing. ASTM abrasion tests showed the importance of the embedment process for limiting the amount of chipping loss. A more specific test using a tribometer (see Fig. 2) was then carried out on a series of wearing course materials. At 20°C, the performance of HPCM was intermediate between conventional bituminous materials and epoxyasphalt materials (concrete or surface dressing). This result is quite satisfactory, given the fact that the temperature should not affect the HPCM behaviour in the 20-50° range, unlike bituminous materials, whose resistance rapidly drops when the temperature increases. Climatic aggressions were simulated through conventional freeze-and-thaw scaling tests, normally devoted to conventional cement concrete. The results obtained led to classify HPCM behavior in the 'very good' category. Then, a more aggressive test called 'total test', encompassing acid attack, freeze-thaw and shocks was carried out. In the absence of a control material, no HPCM classification can be deduced from this last tests. However, it was found that with up to 20 % of chipping loss, the texture characteristics and skid resistance of HPCM are hardly affected, showing the level of safety that can be attained with such a wearing course material.

Miscellaneous

The original texture of a cracking strip was acquired and processed through software aiming at simulating the noise generation likely to occur under traffic. It was found that HPCM should behave as an exposed-aggregate cement concrete of similar texture.

Finally, a key performance test was carried out with the TRL Pavement Testing Facility (TRL, see Fig. 3) including an equivalent of 1.0 M standard axles at 20°C, followed by 0.5 M standard axles at 35°C. This structural test could help in evaluating a pavement structure with various wearing courses, even if the number of loading cycles remained small with regard to the expected traffic for a long-life pavement. Three test pads were tested, covered with HPCM, SMA (stone-mastic asphalt) and EA (epoxyasphalt) concrete, respectively. The loading programme at ambient temperature only provoked a slight level of rutting, which greatly amplified when temperature was raised. The HPCM succeeded in limiting the rutting level to 1.5 mm, although much higher values were attained with the epoxy asphalt (6 mm) and the SMA (8 mm). The HPCM surface remained sound, with a high skid resistance resistance (SRT value of 92). Thin cracking was observed in the two longlife pavement candidate materials, and some delamination happened at the edges of the HPCM pad in the bituminous base course. This distress was due to the rutting of the base course and the lack of tensile strength at 35°C. It was therefore concluded that HPCM had to be applied on a quite stiff asphalt concrete, with a low rutting and a low sensitivity to temperature. These requirements are a direct consequence of the search for a long-life pavement, whatever the wearing course could be.

Conclusion

A new material for a long-life wearing course was developed through a large, collaborative scientific project involving 13 countries, of which 7 were active participants. The main idea for the design of HPCM is the use of best quality materials in minimal quantity. The data acquired in the phase II program are globally encouraging, and one may expect a much longer lifespan, as compared to current asphalt wearing courses (which last generally between 7 and 15 years). The authors are now looking forward to participating in phase III, where practical implementations on trafficked test sections will be carried out. Further research will be necessary during this next phase to develop a suitable construction facility, and to investigate the sensitivity to water dosage and two-dimensional cracking behavior.

Figure 1 .

 1 Figure 1. Testing site for the cracking strips.

Figure 2 .

 2 Figure 2. The 'Tribometer' test, recently developed at LCPC (France)

Figure 3 .

 3 Figure 3. The TRL Pavement Testing Facility (Crowthorne, UK)

Table 1 .

 1 Mixture-proportions of the plain mortar C.

	Components	Kg/m 3
	Siliceous coarse sand 0.2/1	429
	Siliceous fine sand 0.08/0.315	429
	CEM I Portland cement	985
	Silica fume	197
	Superplasticizer (dry powder)	4.40
	Retarder	4.95
	Water	207
	w/c	0.21
	Slump (cm)	21

Table 2 .

 2 Properties of the hardened mortar C with 4% of PVA fibres (fresh state properties: slump 23 cm, air content 4.5 %), after a 28-day curing at 100 % R.H.

	Dimensions of	Type of test	Mean value
	specimens (cm)		(MPa)
	Prisms 4x4x16	Flexural	28.5
	Prisms 4x4x16	Compressive	164
	Cubes 10x10x10	Compressive	148
	Cylinders Ø11x22 E-modulus	43 000
	Cylinders Ø11x22 Compressive	129

Acknowledgements: the SIKA France company is gratefully acknowledged for the advice in the choice of constituents and the delivery of HPCM premix samples to all participants.


David Cachera

Thomas Jensen

Arnaud Jobin

Florent Kirchner

Keywords: Algorithmique, programmation, logiciels et architectures Static Analysis, Automatic Invariant Generation, Abstract Interpretation, Polynomial Invariants, Polynomial Ideals

We propose an abstract interpretation based method to compute polynomial invariants for imperative programs. Our analysis is a backward propagation approach that computes preconditions for equalities like g = 0 to hold at the end of execution. It extends previous work by Müller-Olm and Seidl to a language that includes both polynomial equalities and disequalities. Properties are expressed using ideals, a structure that satisfies the descending chain condition, enabling fixpoints computations to terminate without use of a widening operator. In the general case, termination is characterized using ideal membership tests and Gröbner bases computations. In order to optimize computational complexity, we propose a specialized analysis dealing with inductive invariants which ensures fast termination of fixpoints computations. The optimized procedure has been shown by experiments to work well in practice, and to be two orders of magnitude faster than the state of the art analyzer of Carbonell and Kapur.

Inférence rapide d'invariants polynomiaux pour programmes impératifs

Résumé : Nous proposons une méthode fondée sur la théorie de l'interprétation abstraite pour calculer des invariants polynomiaux de programmes impératifs.

Notre analyse statique suit une approche arrière, qui calcule des préconditions pour qu'une égalité du type g = 0 soit vérifiée à la fin de l'exécution d'un programme. Cette approche étend des travaux précédents de Müller-Olm et Seidl à un langage qui inclut à la fois des égalités et des inégalités polynomiales. Les propriétés sont exprimées à l'aide d'idéaux de polynômes. La propriété de chaîne descendante de l'ensemble des idéaux garantit alors la terminaison des calculs de point fixe sans avoir besoin de faire appel à un opérateur d'élargissement. Dans le cas général, cette terminaison est caractérisée par un test d'inclusion reposant sur le calcul de bases de Gröbner. Afin d'améliorer la complexité, nous proposons une analyse spécialisée dans la découverte d'invariants inductifs, ce qui permet une terminaison rapide des calculs. Les expérimentations que nous avons menées montrent que cette procédure fournit des résultats satisfaisants en pratique, avec un temps de calcul de deux ordres de grandeur plus court qu'un analyseur à l'état de l'art, notamment celui de Carbonell et Kapur.

Mots-clés : Analyse statique, génération automatique d'invariants, interprétation abstraite, invariants polynomiaux, idéaux de polynômes

Introduction

The problem of automatically inferring polynomial (non-linear) invariants of programs is currently one of the major challenges in program verification. This is in contrast to the case for linear invariants where the initial work by Karr [START_REF] Karr | Affine relationships among variables of a program[END_REF] and Cousot and Halbwachs [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] has lead to efficient implementations based on variants of the polyhedral domain. Initial approaches to the non-linear problem proposed extensions of linear techniques [START_REF] Karr | Affine relationships among variables of a program[END_REF][START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] Michael Colón | Linear invariant generation using non-linear constraint solving[END_REF][START_REF] Sankaranarayanan | Constraintbased linear-relations analysis[END_REF] to the non-linear case, made possible by imposing restrictions on the programming language. Sankaranarayanan et al. [START_REF] Sankaranarayanan | Non-linear loop invariant generation using Gröbner bases[END_REF] proposed a constraint-based technique that generates non-linear invariants for programs containing only equality tests. A concomitant approach by Müller-Olm and Seidl [START_REF] Müller | Polynomial constants are decidable[END_REF][START_REF] Müller | Computing polynomial program invariants[END_REF] defines an abstract interpretation method that can generate polynomial invariants for a restrictive class of guarded-loop programs where tests in conditionals are polynomial disequalities. Their analysis is a backward propagation based method: they start from p and compute the weakest preconditions of the satisfiability of the relation p = 0. More precisely, in order to prove that a polynomial relation p = 0 is valid at the end of a program, they show that the set of zeroes of a polynomial p can be exactly abstracted by a polynomial ideal. The restrictions imposed on the language are sufficiently strong to ensure that their method can be proven complete.

Rodríguez-Carbonell and Kapur develop another approach, casting the analysis as an abstract interpretation problem over a domain of ideals of variety. Their approach gave rise to two different procedures. The first one [START_REF] Rodríguez | Automatic generation of polynomial loop invariants: algebraic foundations[END_REF][START_REF] Rodríguez | Program verification using automatic generation of invariants[END_REF][START_REF] Rodríguez | Generating all polynomial invariants in simple loops[END_REF] consists in a complete method for computing all polynomial invariants for a rather restrictive class of programs: it considers simple loops with no conditional tests and whose assignments functions are required to be so called solvable mappings, i.e. a generalization of affine mappings. Thanks to these limitations, the generation procedure is proved to terminate without making use of a widening operator, with a number of iterations bounded by the number of variables of the program. In the second procedure [START_REF] Rodríguez | An abstract interpretation approach for automatic generation of polynomial invariants[END_REF][START_REF] Rodríguez | Automatic generation of polynomial invariants of bounded degree using abstract interpretation[END_REF], these restrictions are removed and programs with polynomial equalities or disequalities guards are considered. As a result, their method is no more complete and may not terminate. To ensure termination, the authors use a widening operator that consists in dynamically removing polynomials of a degree greater than a fixed number. It was an open question at the time whether one could devise an analysis that conciliates both expressiveness and efficiency.

In this paper, we propose an abstract interpretation based method [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] to compute polynomial invariants that has both of the previous properties. Our analysis is a backward propagation approach that extends Müller-Olm and Seidl work [START_REF] Müller | Computing polynomial program invariants[END_REF] to a general polynomial structured programming language that includes if and while constructs where branching conditions are both polynomial equalities and inequalities. As in this previous approach, our analysis uses a form of weakest precondition calculus for showing that a polynomial relation g = 0 holds at the end of a program. Similarly, this verification scheme that applies to a fixed known polynomial can be derived in a generation scheme by using parametrized polynomials. Preconditions are expressed in the mathematical structure of ideals that satisfies the descending chain condition. We show that the backward approach, well adapted to polynomial disequality guards as Müller-Olm and Seidl already noticed, can be extended to equality guards by RR n°7627

1.

y 1 := 0; y 2 := 0; y 3 := x 1 ; 2.

while y 3 = 0 do 3.

if x 2 = y 2 + 1 then 4.

y 1 := y 1 + 1; y 2 := 0; y 3 := y 3 -1; 5. else 6.

y 2 := y 2 + 1; y 3 := y 3 -1; 7.

(a) mannadiv.

1.

x := 0; 2.

y := n; 3.

while y = 0 do 4.

x := x + n; 5.

y := y -1; 6. using polynomial division and greatest fixpoint computations which corresponds to a weakest liberal precondition calculus. Focusing on partial correctness has the consequence that fixpoint iterations in the set of ideals are proved to terminate without the need for a widening operator , as opposed to the general setting of Rodríguez-Carbonell and Kapur. In the general case, termination can be tested by solving the ideal membership problem, namely by Gröbner base computations. In order to reduce computational complexity, we propose a specialized analysis that infers inductive invariants. This restriction, similar to the one made by Sankaranarayanan et al. [START_REF] Sankaranarayanan | Non-linear loop invariant generation using Gröbner bases[END_REF], presents the main advantage of ensuring termination of fixpoint computations in only one iteration. We have shown that it successfully infer invariants on a sizeable set of examples and gives excellent performance results.

The following example demonstrates the salient features of the approach. The algorithm in Figure 1a computes the Euclidean division of x 1 by x 2 [START_REF] Manna | Mathematical Theory of Computation[END_REF].

The invariant computed for this example is non-linear, namely y 1 * x 2 + y 2 + y 3 = x 1 . Finding this invariant requires examining both branchs of the if construct, taking into account the information obtained by the guard. Our method is able to compute such invariants, and the relative simplicity of this example is reflected by the fact that we easily discover it, since we focus on inductive invariants. We thus need only one iteration for computing the invariant, on the contrary to Rodríguez-Carbonell and Kapur's approach that requires an heavier iterating method. Because the analysis by Sankaranarayanan et al. [START_REF] Sankaranarayanan | Non-linear loop invariant generation using Gröbner bases[END_REF] has not been implemented, its performance on this type of programs is unknown.

The rest of the paper is organized as follows. In Section 2, we introduce the mathematical background needed throughout the paper, in particular multivariate polynomial algebra, division and remainder operators and the lattice structure of ideals. Section 3 defines the class of programs we are interested in, namely polynomial programs, as well as their backward collecting semantics. In Section 4, we dive into the analysis by defining the abstract semantics of polynomial programs and prove its correctness w.r.t. the concrete semantics.

Section 5 shows how the abstract semantics is used to automatically generate polynomial invariants. Finally, in Section 6 we propose a heuristic to drastically reduce computational complexity by making a natural assumption on invariants. We report on our implementation through a collection of benchmarks from the litterature.

Preliminaries

Our analysis builds a set of polynomial invariants for a given program. We consider polynomials in R[x 1 , . . . , x m ] where m represents the number of variables of the program1 . In the rest of the paper, we will distinguish between x, element of R m , x i element of R, and x i variable of the program.

A set of polynomial invariants {p 1 = 0, . . . , p s = 0} naturally has an algebraic structure of ideal, as recalled by the following definition.

Definition 1 (Polynomial ideal) A set I ⊆ R[x 1 , . . . , x m ] is a polynomial ideal if it contains 0, is stable under addition (if p 1 , p 2 ∈ I then p 1 + p 2 ∈ I) and stable under external multiplication (if q ∈ R[x 1 , . . . ,
x m ] and p ∈ I then q.p ∈ I). We write I for the set of polynomial ideals of R[x 1 , . . . , x m ], and <S> for the polynomial ideal generated by a set S of polynomials. By definition, <S> is the smallest ideal containing all polynomials of S.

The set I can be given a partial order structure by using the reverse subset inclusion between ideals. The upper bound of a set of polynomial ideals is then the intersection of its elements, while the lower bound is the ideal generated by the union of the elements2 . Definition 2 (Lattice structure of I) Given I and J two polynomial ideals, we define I ♯ J = I J, I ♯ J = <I J> and ⊑ ♯ = ⊇. Operators ♯ and ♯ are extended in a standard fashion to range over sets of polynomial ideals. Equipped with these operators, I is a complete lattice, where the least element is ⊥ ♯ = <1> and the greatest element is ⊤ ♯ = <0>.

One of the main benefit using polynomial ideals is that they are finitely generated. This property is known in the litterature as Hilbert's theorem.

Theorem 1 (Hilbert) Every polynomial ideal I ∈ I is finitely generated, i.e., I = <S> for a finite subset S of I.

A standard result of multivariate polynomial theory states that Hilbert's theorem is equivalent to the fact that the set I satisfies the descending chain condition [START_REF] Cox | Ideals, varieties, and algorithms[END_REF]. This is a key property that will be used to ensure termination of our analysis. Theorem 1 above also exhibits the tight link that exists between invariant sets and ideal structure. We have already seen that an invariant set can naturally be represented as an ideal. Conversely, any polynomial ideal can thus be represented by a finite set of polynomials, that can be seen as an invariant set. Therefore, in the rest of the paper, we will make no difference between an invariant set and the ideal generated by these invariants.

The notion of division on multivariate polynomial ring will play an important role when defining the analysis. Contrary to the univariate case, R[x 1 , . . . , x m ] is not equipped with a Euclidean division. However, it is easy to define a division according to a monomial ordering [START_REF] Cox | Ideals, varieties, and algorithms[END_REF]. In our case, we define a general division operator as follows.

Definition 3 (Division operator, remainder) A division operator div is a function mapping a pair of polynomials (g, p) ∈ R[x 1 , . . . , x m ] 2 to a pair (q, r) ∈ R[x 1 , . . . , x m ] 2 such that g = pq + r. Polynomial r is called the remainder of g by p according to div, and is noted Rem(g, p, div) or only Rem(g, p) if the division operator doesn't need to be explicitly given.

Note that the usual divisions defined by a monomial ordering are division operators.

Finally, our concrete semantics will handle subsets of R m 3 whereas our abstract semantics will deal with polynomial ideals. The link between these two domains is given by the following Galois connection P(R m ) ---→ ← --α γ I :

α : P(R m ) → I X → {u ∈ R[x 1 , . . . , x m ] | ∀x ∈ X, u(x) = 0} γ : I → P(R m ) I → {x ∈ R m | ∀u ∈ I, u(x) = 0} such that ∀X ∈ P(R m ), ∀I ∈ I : X ⊑ γ(I) ⇔ α(X) ⊑ ♯ I.

Syntax and semantics of polynomial programs

Our analysis produces invariants of polynomial programs. We consider a variant of the IMP language [START_REF] Winskel | The Formal Semantics of Programming Languages[END_REF] where assignments are polynomial and conditional tests are polynomial (dis)equalities. where ⊲⊳ stands for = or =. We will also use ⊲⊳ for the negation of ⊲⊳.

The concrete syntax will be decorated by line numbers in the implementation, which are omitted in the abstract syntax above. This language abides to the usual small-step operational semantics (SSOS). We will note →: P × R m → A polynomial is said to be invariant for a program if all its terminating states lead to states that are zeroes of the polynomial.

Definition 6 (Polynomial invariant) A polynomial g ∈ R[x 1 , . . . , x m ] is said to be invariant at the end of a program c if, for all σ ∈ R m , ∃ σ f ∈ R m , c, σ → + σ f ⇒ σ f ∈ γ(g)
Note that, for programs with no terminating state, every polynomial will be invariant, which indicates the absence of information for such programs.

Backward semantics. As standard for abstract interpretation methods, we define a concrete semantics that we will use as an intermediate between the abstract semantics and the usual operational semantics. Its backward formulation will come in handy to prove the correctness of the analysis.

Definition 7 (Backward collecting semantics (BCS))

B ν c : P(R m ) → P(R m ) B ν x j := p S = {x ∈ R m | x[ [p(x)] ] j ∈ S} where x[ [p(x)] ] j is the element (x 1 , . . . , x j-1 , p(x), x j+1 , . . . , x m ) B ν skip S = S B ν c 1 ; c 2 S = B ν c 1 (B ν c 2 S) B ν if p ⊲⊳ 0 then c 1 else c 2 S = (B ν c 1 S p ⊲⊳ 0 ) (B ν c 2 S p ⊲⊳ 0 ) where p ⊲⊳ 0 = {x ∈ R m | p(x) ⊲⊳ 0} B ν while p ⊲⊳ 0 do c S = νF c,p,S where F c,p,S = λX.( p ⊲⊳ 0 S) ( p ⊲⊳ 0 B ν c X)
Remark that this intermediate semantics has a greatest fixpoint definition. Compared to a least fixpoint, this provides less information, but the extra information a least fixpoint would give has to do with termination and is not essential to our analysis. In other words, we only deal with partial correctness.

In order to investigate this issue, define the operator B µ . by replacing greatest fixpoint computations by least fixpoints, and consider the following example.

Computing B µ small and B ν small . The program in Figure 1b computes the square of a natural number n by successively adding the content of the variable n to a variable x initially containing 0. Thus, the polynomial g = xn 2 is invariant at the end of the program. The weakest precondition of relation g = 0 holding at the end of the program is given by B µ small γ(g). We start by computing B µ while y = 0 do x := x + n; y := y -1 γ(g), obtaining the least fixpoint by iterating the function

F = λX.( y = 0 γ(g)) ( y = 0 B µ c X) from {}. B µ while y = 0 do x := x + n; y := y -1 γ(g) = k≥0 F k ({}) where F k ({}) = {(x, y, n) ∈ R 3 | (y = 0 ∧ x = n 2 ) ∨ (y = 1 ∧ x + n = n 2 ) ∨ . . . ∨ (y = k ∧ x + kn = n 2 )} Thus, we have B µ small γ(g) = B µ x := 0; y := n ( k≥0 F k ({}) ) = {(x, y, n) ∈ R 3 | ∃k ∈ N such that (0, n, n) ∈ F k ({})} = {(x, y, n) ∈ R 3 | ∃k ∈ N such that n = k} = R × R × N This proves that, if initial condition σ i = (x, y, n) ∈ R × R × N is satisfied,
we eventually reach the end of the program in a state σ f such that g(σ f ) = 0. Condition x ∈ R can easily be expressed with a polynomial (as {x ∈ R | 0 = 0}).

On the contrary, n ∈ N needs an infinite polynomial product to be expressed in

R (as {n ∈ R | k≥0 (n -k) = 0}
) which would make our analysis diverge.

On the other hand, we have B ν small γ(g) = R 3 . This computation is an over-approximation of the least fixpoint and its knowledge may seem not to bring information. However, this must be read as: "relation g = 0 holds for every final states under no initial condition".

To sum up, a least fixpoint computation provides very precise information including termination conditions that have to be fulfilled for the invariant to hold at the end of the program. On the contrary, greatest fixpoint computations brings less precise but more relevant information : it reverses the point of view by focusing on relations satisfied by only final states. We traduce these practical observations in a formal way in the following paragraph.

Comparing backward semantics with SSOS. In order to stress the termination condition implicitly expressed in our concrete semantics, we compare least and greatest fixpoint definitions to SSOS. Theorem 2 states that least fixpoint semantics collects all terminating states. Theorem 2 (B µ . vs SSOS) For all S ∈ P(R m ) and for all polynomial pro-

gram state σ ∈ R m , σ ∈ B µ c S ⇔ ∃σ f ∈ S, c, σ → + σ f
The greatest fixpoint semantics also contains the set of terminating states but may also contains non-terminating ones.

Theorem 3 (B ν . vs SSOS) For all S ∈ P(R m ) and for all polynomial pro-

gram state σ ∈ R m , σ ∈ B ν c S ⇒ ∃σ f ∈ S, c, σ → + σ f or c, σ → ∞
The proofs of both theorems can be found in Appendix A.1. Obviously, if we only consider terminating programs, there is no difference between B µ . and B ν . .

Abstract semantics

The fundamental idea behind abstraction is to correctly export concrete analysis in a coarser world were computations are easier. In our case, the concrete semantics is not computable because of the presence of fixpoint computations in the infinite lattice R m that does not satisfy the ascending chain condition. In this section, we propose an abstract semantics that approximates the concrete semantics and whose underlying workset is I, the set of polynomials ideals. As I is a lattice satisfying the descending chain condition, greatest fixpoints are computable.

We begin by defining the abstract semantics of polynomial programs and then prove that this abstraction correctly approximates the concrete semantics.

Definition 8 (Abstraction of polynomial programs) A few comments on this semantics: first, note that as our analysis acts backward, assignment-semantics only consists in a substitution and does not require the use of fresh variables. Let us elaborate on the presence of the Remoperator in the semantics of the if construct. Considering an if statement guarded by a (dis)equality p, this semantics is based on the following simple idea: if we want to prove that relation g = 0 holds and we know that relation p = 0 holds, it suffices to compute Rem(g, p) = g -pq for a certain polynomial q and to prove that relation Rem(g, p) = 0 holds. We point out that this property does not depend on the choice of q; in particular, this choice does not impact the correctness of our approach. However, some choices are not really relevant and may later lead to the generation of the trivial invariant "0 = 0". Additional details on how to find a suitable division operator are given in Section 6.

c ♯ : I → I x j := p ♯ I = {q[ [x j → p] ], q ∈ I} where q[ [x j → p] ] is the polynomial q(x 1 , . . . , x j-1 , p(x 1 , . . . , x m ), x j+1 , . . . , x m ) skip ♯ I = I s 1 ; s 2 ♯ I = s 1 ♯ ( s 2 ♯ I) if p = 0 then c 1 else c 2 ♯ I = <p.( c 1 ♯ I), Rem( c 2 ♯ I, p)> if p = 0 then c 1 else c 2 ♯ I = <p.( c 2 ♯ I), Rem( c 1 ♯ I, p
Remark 1 In the special case of a program c ≡ if p = 0 then c 1 else skip, the best choice for a quotient is given by q = 0, which defines Rem(g, p) = g. The abstract semantics of c is then given by c ♯ I = <I, p.( c 1 ♯ I)>. This coincides with Müller-Olm and Seidl's abstract function, which is proven to be an exact abstraction of the concrete transfer function [START_REF] Müller | Computing polynomial program invariants[END_REF].

The semantics for while is derived from that of if . Note that, similarly to the concrete semantics, it is defined by a greatest fixpoint definition. The RR n°7627 abstract transfer function for while is computed with a Kleene fixpoint iteration starting from ⊤ ♯ = <0>, the top element of the lattice I. More precisely, for all V ∈ I,

while p = 0 do c ♯ V = ♯ n≥0 (F ♯ c,p,V ) n (⊤ ♯ )
According to Theorem 1, this iteration terminates in finitely many steps. As {(F ♯ c,p,V ) n (<0>)} n∈N is an increasing sequence 4 , the stopping criterion consists in checking if the polynomials at step n + 1 belong to the ideal generated at step n. Note that this ideal membership problem is decidable thanks to Gröbner base computations [START_REF] Cox | Ideals, varieties, and algorithms[END_REF]. As incremental computations are involved here, we propose to use Faugère's F 5 algorithm to this purpose [START_REF] Faugère | A new efficient algorithm for computing Gröbner bases without reduction to zero (F5)[END_REF].

Remark 2 As the abstract transfer function for while is derived from c ≡ if p = 0 then c 1 else skip, and following Remark 1, the abstract definition of a while statement guarded by a polynomial disequality is given by the trivial division operator that leaves its argument unchanged. This simplifies the definition of F ♯ c,p,I into λJ.<p.( c ♯ J), I>.

Correctness of the analysis. We now have to prove that our abstract semantics is correct with respect to the concrete one. Both semantics are compared using the Galois connexion defined in Section 2.

Theorem 4 (Correctness) Let g be a polynomial and c a polynomial program. Then:

γ( c ♯ <g>) ⊆ B ν c γ<g>
We prove Theorem 4 by induction on the syntax of polynomial programs. The complete proof can be found in Appendix B. Note that this theorem, and its corollary hereafter, are key to show that our analysis indeed generates polynomial invariants.

Corollary 1 Let g be a polynomial in R[x 1 , . . . , x m ] and c a polynomial program. If g satisfies c ♯ <g> = <0>, then g is a polynomial invariant at the end of c.

Proof. For a given polynomial g,

if c ♯ <g> = <0>, then γ( c ♯ <g>) = R m . As γ( c ♯ <g>) ⊆ B ν c γ<g>, we have B ν c γ<g> ⊇ R m , which proves that B ν c γ<g> = R m .
Using Theorem 3, this implies that, for any initial state σ ∈ R m , if there exists σ f such that c, σ → + σ f , then σ f ∈ γ(g). Thus, g is a polynomial invariant. ⊓ ⊔ Corollary 1 provides a method to verify that a given polynomial g is invariant. It consists in computing the abstract semantics on <g> and comparing the result with the zero ideal <0>. In the next section, we will show how to use Corollary 1 to generate polynomial invariants.

Generating polynomial invariants

As noticed with Corollary 1, the abstract semantics naturally provides a way to validate an invariant candidate. We now show how the additional use of parametrized polynomials allows for automatically generating invariants. Definition 9 (linear a i -parametrized polynomial) We denote by a i (i ∈ N) a set of parameters. A polynomial g ∈ R[x 1 , . . . , x m ] is said to be a linear a i -parametrized polynomial (noted a i -lpp) if its coefficients are a linear combination of the a i -parameters. For example, a 0 + a

1 .x 1 + a 2 .x 2 + a 3 .x 1 x 2 + a 4 .x 1 2 + a 5 .x 2
2 is the most generic linear a i -parametrized polynomial of R[x 1 , x 2 ] of degree 2. An ideal is said to be a linear a i -parametrized ideal if it is generated by linear a i -parametrized polynomials. Line 4 brings up the most significant difference with the verification scheme detailled by Corollary 1. Indeed, as we start from an a i -lpp polynomial, c ♯ <g> is a set of parametrized polynomials. More precisely, we can show by induction on the syntax of polynomial programs that c ♯ <g> is a linear a i -parametrized ideal. Now, proving that equality c ♯ <g> = <0> holds is equivalent to proving that all polynomials in c ♯ <g> are null. As a polynomial is null if all its coefficients are null, C g,c contains the coefficients of all polynomials in c ♯ <g>. These coefficients are linear combination of the a i parameters. Thus, C g,c is an homogeneous system of a i -linear equations, and S g,c can be obtained by a simple Gaussian elimination algorithm. Thanks to S g,c , each a i can be rewritten into a linear combination of a subset of the initial parameters, that corresponds to a basis of the linear system. Similarly, the a i -lpp polynomial g is rewritten using this same basis, yielding the parametrized polynomial g. The remaining a i s being left unconstrained, any instantiation of these parameters constitute a program invariant: these instantiations form the set G. These remarks are summarized in the following correctness theorem. An important remark here is that generating C g,c can be costly, as the stopping criterion requires computing Gröbner bases on parametrized polynomials. We are exploring several avenues to deal with this complexity in the general case, starting with naïvely capping the number of iterations. This would allow us to produce polynomial invariant candidates, which are simpler to verify. In the next section, we propose another way to cope with this complexity issue. By making a natural assumption on the polynomial relations we want to generate, we prove that only one iteration suffices to compute fixpoints for while statements guarded by a polynomial disequality.

1. r := 0; 2. s := 1; 3. t := 1; 4. while s ≤ n do 5.

r := r + 1; 6.

t := t + 2; 7.

s := s + t; 8.

I1 I4[ 1 /t; 1 /s; 0 /r] I4 I8 ♯ I 1 5 ♯ I 2 5 ♯ I 3 5 ♯ I 4 5 ♯ I 5 5 I 1 5 <a0 +a1(r +1)+a2(s+t+2)+a3(t+2)+a4n+ a5(r+1) 2 +a6(r+1)(s+t+2)+a7(r+1)(t+2)+ a8(r+1)n+a9(s+t+2) 2 +a10(s+t+2)(t+2)+ a11(s+t+2)n+a12(t+2) 2 +a13(t+2)n+a14n 2 > I8 <a0 + a1r + a2s + a3t + a4n + a5r + a6rs + a7rt + a8rn + a9s 2 + a10st + a11sn + a12t 2 + a13tn + a14n 2 >
Figure 2: A polynomial program to compute a square root: sqrt.

Example 1 (invariant for sqrt) In this paragraph, we illustrate Algorithm 1 on the small and didactic example of Figure 2. We deliberately make the choice of a simple example, where the guard is not taken into account, to be able to display each step of Algorithm 1. The table on the right of Figure 2 contains key abstract values of the analysis. In this example, we aim at computing invariants of degree less than or equal to 2. Note that this is not indicative of a limitation of the analysis, which is in no way bound to the quadratic case. Examples in Section 6 deal with full guards and higher-degree invariants. Abstract computations start from ideal I 8 that only contains g, the most generic a i -lpp polynomial of degree 2 in variables r, s, t, n. As the guard of the while statement is not a polynomial (dis)equality, it is replaced by a non deterministic choice, and the loop is unfolded until a fixpoint is reached. I 4 = while ( * ) do r := r + 1; t := t + 2; s := s + t ♯ g = <g, g 1 , g 2 , g 3 , . . . > where g i corresponds to the polynomial computed on line 5 at step i (g 0 = g and for i ≥ 1, g i = I i 5 = r := r + 1; t := t + 2; s := s + t ♯ (g i-1 )). By Theorem 1, we know that this iteration terminates in finitely many steps. Gröbner bases computation show that g 6 ∈ <g, g 1 , g 2 , g 3 , g 4 , g 5 >, which is sufficient to prove that I 4 = <g, g 1 , g 2 , g 3 , g 4 , g 5 >. Finally, I 1 is built by substituting the program variables in I 4 by the values given by the initial assignments. The next step of Algorithm 1 consists in obtaining the linear constraints equivalent to equality I 1 = <0>. For example, the constraint a 0 +a 2 +a 3 +a 9 +a 10 +a 12 = 0 is obtained by equating the coefficient of degree 0 in g[ 1 / t ; 1 / s ; 0 / r ] to zero. For lack of space, we do not detail the whole linear system and skip directly to the computation of its solution (line 5 of Algorithm 1). Taking the set {a 0 , a 2 , a 7 , a 10 , a 12 } as basis parameters yields

S g,sqrt =      a1 = 2a0 -a7 -2a12 a6 = -2a10 a3 = -a0 -a2 -a10 -a12 a8 = -2a13 a4 = -a13 a9 = a11 = a14 = 0 a5 = -a2 -2a7 -a10 -4a12
Substituting the a i -parameters according to this solution, we conclude that, for all a 0 , a 2 , a 7 , a 10 , a 12 ∈ R

a0(1 + 2r -t) + a2(s -t -r 2 ) + a7(-r -2r 2 + rt) + a10(-t -r 2 -2rs + st) + a12(-2r -t -4r 2 + t 2 ) + a13(-n -2rn + tn) = 0
Each polynomial that appears after parameters a 0 , . . . , a 13 in this formula is invariant at the end of program sqrt. These invariants are subsumed by t = 2r + 1 and s = (r + 1) 2 .

RR n°7627

As already noticed, the use of Gröbner base computations to decide termination can be avoided in certain cases, while retaining the precision of our approach. The following Section explores a subclass of program invariants, on which termination is obtained in a single iteration step.

Fast generation of inductive invariants for loops

The basic idea for accelerating convergence consists in restricting the set of invariant candidates by making a natural assumption: an invariant g is said to be inductive for a loop if the relation g = 0 is satisfied at the beginning of the loop and remains true when iterating.

Definition 10 (Inductive (loop) invariants) Let us consider a loop program w ≡ while b do c. An invariant is said to be inductive for w if, for all σ in γ(g), if there exists σ ′ ∈ R m such that c, σ → + σ ′ , then σ ′ ∈ γ(g).

This definition can be rewritten using the backward concrete semantics, as stated by the following lemma, which is a direct consequence of Theorem 3.

Lemma 1 Let w ≡ while b do c be a polynomial loop program and g a polynomial in R[x 1 , . . . , x m ]. Then, g is an inductive invariant for w if and only if γ(g) ⊆ B ν c γ(g).

The notion of inductive invariant now has to be translated into the abstract semantics. The following theorem gives a sufficient condition for having an inductive invariant.

Theorem 6 (Inductive hypothesis) Assuming the notations of Lemma 1, if c ♯ <g> = <g>, then g is an inductive invariant.

Proof. By Theorem 4, we have γ( c ♯ <g>) ⊆ B ν c γ<g>. Hypothesis c ♯ g = <g> and Lemma 1 allow to conclude the proof. ⊓ ⊔ This theorem has a direct consequence on fixpoint computations: by positing the inductive hypothesis, we can prove that iterating is not needed to compute abstract while statements guarded by a polynomial disequality.

Lemma 2 Let g ∈ P and w ≡ while p = 0 do c be a polynomial loop program. Suppose that c ♯ <g> = <g>. Then w ♯ <g> = <g>.

Proof. According to Remark 2, we have while p = 0 do c ♯ <g> = <g, p.( c ♯ g), . . . > By hypothesis, c ♯ <g> = <g>. Thus, p.( c ♯ <g>) = p<g> ⊆ <g>, which proves that stabilization is reached and concludes the proof. ⊓ ⊔ In the case of loops wih positive guards, the analysis still needs to iterate through the successive remainder computations. The termination of this process is still ensured by the descending chain property of polynomial ideals, and the analysis proceeds as in the general case of Section 4. An alternative is to overapproximate the solution set by treating positive guards nondeterministically; this brings us back to the quick single iteration case. In practice however, positive guarded loops are a rare occurrence: for instance, none of Carbonell and Kapur's polynomial program benchmarks [START_REF] Rodríguez | Automatic generation of polynomial invariants of bounded degree using abstract interpretation[END_REF][START_REF] Rodríguez | Generating all polynomial invariants in simple loops[END_REF] include such conditionals.

The following example illustrates two important points: it explains the Remcomputations and demonstrates the use of the inductive hypothesis.

Example 2 (inductive invariant for mannadiv) Recall algorithm from Figure 1a. As in Section 5, we call I i the ideal generated from unfolding the semantics of the instruction at line i. The analysis starts from ideal I 7 = <g>, containing the most generic quadratic a i -lpp polynomial g, and performs a series of variable instantiations before evaluating the if instruction of line 3. We note g 1 = g[ y3-1 / y3 ; 0 / y2 ; y1+1 / y1 ] and g 2 = g[ y3-1 / y3 ; y2+1 / y2 ] the polynomials produced by these instantiations. Ideal I 3 is defined using the operation Rem(g 1 , p) where p = x 2 -y 2 -1. As already mentioned in Section 4, the choice of the division operator is crucial for our analysis and a bad choice may lead to a loss of precision. To avoid this issue, we perform division by a parametrized polynomial. In this example, computation of Rem(g 1 , p) is done as follows. We introduce q the most generic b i -lpp of degree deg(g 1 ) -deg(p) = 1, and define

Rem(g 1 , p) = g 1 -q.p = g 1 -(b 0 + b 1 x 1 + b 2 x 2 + b 3 y 1 + b 4 y 2 + b 5 y 3 ).(x 2 -y 2 -1)
Note that the resulting polynomial is in {a i , b i }-lpp form, which is essential for the linearity of the constraints generated further. Ideal I 3 = <(x 2 -y 2 -1).g 2 , Rem(g 1 , p)> is then built from this definition.

The while instruction from line 2 triggers the use of the inductive hypothesis (Theorem 6), indicating that the loop body maintains the original invariant, constraining I 3 to be equal to I 7 . This constraint can be satisfied by enforcing both Rem(g 1 , p) = g and g 2 = g. Let C w1 and C w2 be these respective constraints. What is more, by Lemma 2 we have I 2 = I 7 . The substitutions on line 1 operate on I 2 ; enforcing the nullness of I 1 generates another set of constraints C i . The important point here is that the constraints C w * and C i express two different properties of the invariant (inductiveness, and initial nullness), and that solving only C i would yield an incomplete solution.

Step 4 of Algorithm 1 consists in solving the conjunct of all constraints:

Ci Cw 2 Cw 1 a6 + a10 + a20 = 0 a20 = a18 a10 = a8 a18 + a13 = 0 a1 + a5 = 0 a19 = 2 a18 a20 = a15 a9 = a16 = a19 = 0 a7 + a14 = 0 a17 = a16 b4 + a13 = 0 b1 = b2 = b3 = b5 = 0 a0 = a2 = a11 = 0 a4 = a5 b0 = a12 -a14 a10 = a9 a5 = a3 -a14 + a12 a7 + a14 a4 = a12 -a13 -a14 a14 = a13 a17 = 2 a15
These resolve into a 12 = a 5 = a 4 = b 0 = -a 1 , and all other parameters equating to 0. Finally, the direct instantiation of the a i -lpp polynomial returns the single program invariant:

x 1 = y 1 x 2 + y 2 + y 3 .
Examples and benchmarks. Table 3 presents the results of the Maple implementation of our analysis. It is run on Rodríguez-Carbonell and Kapur's inductive benchmarks [START_REF] Rodríguez | Generating all polynomial invariants in simple loops[END_REF][START_REF] Rodríguez | Automatic generation of polynomial invariants of bounded degree using abstract interpretation[END_REF], and measured to their best and worst results. Our method is systematically better, and on average 2. that yields an invariant of degree 31, and run cohencu and freire2 with a different set of parameters in order to find a more interesting, higher-order invariant (resp. x = n 3 , and 4r 3 -6r 2 + 3r + 4x -4a = 1). Our analysis had more mixed results with the knuth program: we had to introduce two additional variables to encode the non-polynomial initial assignements, which significantly increased the size of the linear system. It is unclear how Rodríguez-Carbonell and Kapur dealt with these assignments. Unfortunately, we were not able to compare to Sankaranarayanan et al.' s approach, for lack of an implementation. An OCaml implementation of this analysis for Java bytecode, using the Sawja5 static analysis libraries to derive annotations and intermediate code representation, provides a fully automated invariant generation tool. Early results have been competitive with the Maple implementation, and a prototype is available at www.irisa.fr/celtique/ext/polyinv. A thorough analysis of our results can be found in Appendix C.

Related work

As already mentioned in the introduction of this paper, our approach extends Müller-Olm and Seidl's work [START_REF] Müller | Computing polynomial program invariants[END_REF] to a structured language with both polynomial equality and disequality guards. In the case of programs with negative guards only, our abstract function coincides with theirs, thus inheriting the completeness property. In terms of computational complexity, we propose a practical alternative to iteration-based methods, by extending the hypotheses of Sankaranarayanan et al. [START_REF] Sankaranarayanan | Non-linear loop invariant generation using Gröbner bases[END_REF] to a more general setting without sacrificing efficiency. More precisely, the condition c ♯ <g> = g, which provides the most efficient invariant computation, corresponds to their notion of constant value consecution, and the condition c ♯ <g> = <g>, which is the inductive hypothesis of Theorem 6, corresponds to their notion of constant-scale consecution.

Rodríguez-Carbonell and Kapur [START_REF] Rodríguez | Automatic generation of polynomial invariants of bounded degree using abstract interpretation[END_REF] propose a method adapted to both kinds of guards, but at the price of a high degree of computational and conceptual complexity. First, their abstract domain is the set of ideal varieties, i.e., ideals such that α • γ(I) = I (called the IV property). The transfer function for disequality guards comes down to computing ideal quotients in this abstract domain. The IV property is costly to maintain, since it relies on the computation of radical ideals. By default, their implementation skips these computations and ignores disequality guards, thus inducing over-approximations. In their forward approach, abstract assignments are handled by fresh variable introduction and elimination. This requires computing ideal intersections. Abstract equality tests, which are easier to handle in a forward approach, still need IV computations due to the nature of the abstract domain. These are also generally skipped in practice. Finally, even if their approach can be adapted to bound the number of iterations by making strong assumptions on programs [START_REF] Rodríguez | Generating all polynomial invariants in simple loops[END_REF], it systematically demands iterative fixpoint computations. The process of computing all polynomial invariants for a given structure of programs was extended by Kovács in [START_REF] Kovács | A complete invariant generation approach for P-solvable loops[END_REF] which provides, again through iterative fixpoint computation, a complete invariant generation method for a specific loop pattern with nested conditionals.

Conclusion

We have presented a backwards polynomial invariant generation method that enjoys both programming language expressiveness and, for a large class of invariants, a fast generation procedure.

The proposed method constitutes a solid foundation for extensions to an analysis tool that covers a full-fledged language, such as the Java bytecode. The analysis has good scalability properties as the limiting factor is the number of variables and not the degree of the variables nor the size of the code. The integration of the analysis into the Sawja static analysis framework for Java yields good results on benchmarks from the litterature and will enable us to back these claims with experiments on large code bases.

In addition, there are at least two specific avenues we will investigate in further work. For one, the non inductive invariant generation case still requires Gröbner bases computation in order to know when loop unfolding has to be stopped. We are currently experimenting to identify which kind of algorithm is well adapted to our particular form of ideals. Second, on a more theoretical side, the abstract transfer functions for handling our if and while control structures are based on remainder computations, where any remainder function yields a correct abstract semantics. We have found a way to implicitly generate "good" remainder functions for inductive invariants, but an exact characterization of such functions in the general case is still to be found.

We also undertook the mechanized formalization of all the material of this paper with the Coq proof assistant, following Besson et al.'s approach [START_REF] Besson | Certified result checking for polyhedral analysis of bytecode programs[END_REF] to linear invariant generation. In addition to the gain in confidence, this lays the groundwork for a certifying analysis toolchain, i.e., the combination of an analyzer that generates certificates in predefined format, and a formally verified checker that validates them.

RR n°7627 seq c 1 ; c 2 , σ ∼ c 2 , c 1 , σ σ → σ ′ congruence c, σ → c, σ ′ skip skip, σ → σ p(σ) = v assign x j := p, σ → σ[ [v] ] j p(σ) ⊲⊳ 0 ≡ true if if p ⊲⊳ 0 then c 1 else c 2 , σ → c 1 , σ where 0 = 0 v = 0 ≡ true p(σ) ⊲⊳ 0 ≡ false if if p ⊲⊳ 0 then c 1 else c 2 , σ → c 2 , σ where 0 = 0 v = 0 ≡

A Semantical Frameworks and Relations

A.1 Wright-Felleisen small-step semantics of polynomial programs.

The semantics of polynomial programs is defined as a relation between closed terms c. We use a congruence rule to lift the primitive deduction rules to a standard, left-to-right, innermost-to-outermost interpretation of the language.

Definition 11 (Small-step operational semantics (SSOS)) Let c be a polynomial program, v a program value, and σ, σ ′ ∈ R m be states of the program c.

The reduction semantics of our language is provided by the rules in Figure 4.

Remark that we use the ∼ relation to denote macro-like expansion. We use this notation to refrain from introducing additional steps in the small-step reductions.

A.2 Relation between backward and operational semantics

A.2.1 Comparing B µ . with SSOS.

We begin by comparing the backward least fixpoint collecting semantics B µ . with SSOS. Theorem 7 states that least fixpoint semantics collects all terminating states.

Theorem 7 (B µ . vs SSOS) For all S ∈ P(R m ) and for all polynomial program state σ, σ ∈ B µ c S ⇔ ∃σ f ∈ S, c, σ → + σ f First, remark that, according to the definition of the SSOS, there is no program c and states σ, σ f ∈ R m such that c, σ → 0 σ f . Thus, if c, σ → * σ f is satisfied for σ, σ f ∈ R m then c, σ → + σ f . This property will be used in further proofs without mentioning it.

In order to improve the readability of Theorem 7, we divide it in two lemmas stating one or the other side of the equivalence.

If c ≡ if p ⊲⊳ 0 then c 1 else c 2 Recall B µ c S = ( p ⊲⊳ 0 B µ c 1 S) ( p ⊲⊳ 0 B µ c 2 S).
Assume p(σ) ⊲⊳ 0 ≡ true then c, σ → 1 c 1 , σ → m σ f . By induction hypothesis, we get σ ∈ B µ c 1 S. Thus, σ ∈ p ⊲⊳ 0 B µ c 1 S and as a consequence σ ∈ B µ c S.

Assume p(σ) ⊲⊳ 0 ≡ f alse then c, σ → 1 c 2 , σ → m σ f . By induction hypothesis, we get σ ∈ B µ c 2 S. Thus, σ ∈ p ⊲⊳ 0 B µ c 2 S and as a consequence σ ∈ B µ c S.

Thus the property holds for this case.

RR n°7627

either p(σ) ⊲⊳ 0 ≡ true thus σ ∈ B µ c 1 S. The induction hypothesis states ∃σ ′ ∈ S, c 1 , σ → + σ ′ . And the small-step semantics provides the step:

p(σ) ⊲⊳ 0 ≡ true if if p ⊲⊳ 0 then c 1 else c 2 , σ → c 1 , σ
or p(σ) ⊲⊳ 0 ≡ false is the mirror case: take σ ∈ B µ c 2 S. The induction hypothesis states ∃σ ′ ∈ S, c 2 , σ → + σ ′ . What is more:

p(σ) ⊲⊳ 0 ≡ false if if p ⊲⊳ 0 then c 1 else c 2 , σ → c 2 , σ Thus, σ f = σ ′ and c, σ → + σ ′ .
If c ≡ while p ⊲⊳ 0 do c 1 then we have, using the Kleene iteration theorem:

B µ c S = µF c1,p,S = n≥0 F n c1,p,S ({})
Now consider σ ∈ B µ c S; thus, ∃n 0 ∈ N such that σ ∈ F n0 c1,p,S ({}). To conclude this case, we prove by mathematical induction that:

∀n ∈ N, σ ∈ F n c1,p,S ({}) ⇒ ∃σ f ∈ S, c, σ → + σ f • Case n = 0. As F 0
c1,p,S ({}) = {}, the implication is valid because its premise is false.

• n → n + 1. Let n ∈ N such that σ ∈ F n c1,p,S ({}) ⇒ ∃σ f ∈ S, c 1 , σ → + σ f . Let now suppose that σ ∈ F n+1 c1,p,S ({}). We have: either p(σ) ⊲⊳ 0 ≡ false then after macro expansion, the small-step semantics provides the step:

F n+1 c1,
p(σ) ⊲⊳ 0 ≡ false if c, σ → skip, σ
Thus σ f = σ and c, σ → + σ f . or p(σ) ⊲⊳ 0 ≡ true then σ ∈ B µ c 1 (F n c1,p,S ({})). By induction hypothesis on c 1 , there exists σ ′′ such that c 1 , σ → + σ ′′ , and by induction hypothesis on n, we get that c 1 , σ ′′ → + σ f . What is more:

p(σ) ⊲⊳ 0 ≡ true if c, σ → c 1 ; c, σ Thus, c, σ → + σ f .
This proves that the property holds for this last case and thus always holds.

⊓ ⊔

RR n°7627

A.2.2 Comparing SSOS with B ν . .

The greatest fixpoint semantics also contains the set of terminating states but may also contains non-terminating states, putting aside termination condition.

Theorem 8 (B ν . vs SSOS) For all S ∈ P(R m ) and for all polynomial program state σ,

σ ∈ B ν c S ⇒ ∃σ f ∈ S, c, σ → + σ f or c, σ → ∞
Proof. By syntactic induction on the polynomial program c. We proceed by case.

If c ≡ skip then we have both B ν c S = S, and for all σ ∈ R m ,

skip skip, σ → σ which holds, a fortiori, for σ ∈ B ν c S ⊆ R m . Thus we have σ f = σ. If c ≡ x j := p then we have both B ν c S = {x ∈ R m | x[ [p(x)] ] j ∈ S}, and for all σ ∈ R m , p(σ) = v assign x j := p, σ → σ[ [v] ] j where σ[ [v] ] j = (σ 1 , . . . , σ j-1 , v, σ j+1 , . . . , σ m ) Thus we have σ f = σ[ [v] ] j . If c ≡ c 1 ; c 2 then we have B ν c 1 ; c 2 S = B ν c 1 (B ν c 2 S)
By induction hypothesis, we have:

1. σ ′ ∈ B ν c 2 S ⇒ ∃σ ′′ ∈ S, c 2 , σ ′ → + σ ′′ or c 2 , σ ′ → ∞ 2. σ ∈ B ν c 1 (B ν c 2 S) ⇒ ∃σ ′ ∈ B ν c 2 S, c 1 , σ → + σ ′ or c 1 , σ → ∞
Thus the compound application of the seq and congruence rules yields the following derivation tree:

c 1 ; c 2 , σ ✲ 1 c 2 , c 1 , σ ✲ + c 2 , σ ′ ✲ + σ ′′ ∞ ✲ ∞ ✲ Hence, either c diverges, or σ f = σ ′′ .
If c ≡ if p ⊲⊳ 0 then c 1 else c 2 then we have:

B ν c S = (B ν c 1 S p ⊲⊳ 0 ) (B ν c 2 S p ⊲⊳ 0 )
Now consider σ ∈ B ν c S; two cases arise:

RR n°7627 ambiguity, we can formally define j .F i by the following recurrence:

                   0 .F 1 = p ⊲⊳ 0 S j .F j+1 = p ⊲⊳ 0 B ν c 1 ( j-1 .F j ), ∀j ≥ 1 1 .F 1 = p ⊲⊳ 0 B ν c 1 (R m ) j .F j = p ⊲⊳ 0 B ν c 1 ( j-1 .F j-1 ), ∀j ≥ 2 t .F j+1 = t .F t+1 , ∀1 ≤ t ≤ j
The proof is based on the following idea. If we are able to find a derivation of c, σ that reaches the set p ⊲⊳ 0 , then, by unfolding the loop once more, we make this derivation terminate in one more step. This case is characterized by the fact that σ belongs to a t .F i for a 0 ≤ t ≤ i -1. Note that, thanks to the last line of the above recurrence, this property can be reformulated as σ ∈ i-1 .F i for a certain i ≥ 1. If we can't find such a derivation, it means that we keep infinitely deriving in the set p ⊲⊳ 0 and never leave the loop. This case is characterized by the fact that for all i ≥ 1, σ belongs to i .F i . Note that either one of this characterization is realized. The rest of the proof consists in formalizing this idea.

The following lemma expresses what occurs if the first case is satisfied.

Lemma 5 (First case) Let c ≡ while p ⊲⊳ 0 do c 1 . Then, ∀σ ∈ R m , ∀j ≥ 1, σ ∈ j-1 .F j ⇒ ∃σ f ∈ S, c, σ → + σ f or c, σ → ∞ Proof. By recurrence on j. Let σ ∈ R m . • If j = 1. Then σ ∈ 0 .F 1 = p ⊲⊳ 0 S and p(σ) ⊲⊳ 0 ≡ false if c, σ → σ Defining σ f = σ concludes this case.
• Suppose that property holds at rank j and let σ ∈ j .F j+1 = p ⊲⊳ 0 B ν c 1 ( j-1 .F j ). Then, we have

p(σ) ⊲⊳ 0 ≡ true if c, σ → (c 1 ; c), σ and finally c 1 ; c, σ ∼ c, c 1 , σ ✲ + c, σ ′ ✲ + σ ′′ ∞ ✲ ∞ ✲
First step is just a macro expansion. Second step is the result of syntactic induction: as σ ∈ j .F j+1 ⊆ B ν c 1 ( j-1 .F j ), either there exists a state σ ′ such that σ ′ ∈ j-1 .F j and c 1 , σ → + σ ′ or c 1 , σ → ∞ . The final step results from the recurrence hypothesis. Defining σ f = σ ′′ concludes this case.

⊓ ⊔

The second case is treated with help to the following lemma.

Lemma 6 (Second case) Let c ≡ while p ⊲⊳ 0 do c 1 . Then,

∀σ ∈ R m , ∀j ≥ 1, σ ∈ j .F j ⇒ ∃i j ≥ j -1, σ ′ ∈ p ⊲⊳ 0 , c, σ → ij c, σ ′ or c, σ → ∞ Proof. By recurrence on j. Let σ ∈ R m . • If j = 1. Then σ ∈ 1 .F 1 = p ⊲⊳ 0 B ν prog 1 (R m ).
As c, σ → 0 c, σ , defining σ ′ = σ concludes the case.

• Suppose that property holds at rank j and let σ ∈ j+1 .F j+1 = p ⊲⊳ 0 B ν c 1 ( j .F j ). Then, we have

p(σ) ⊲⊳ 0 ≡ true if c, σ → (c 1 ; c), σ
which provides, as in the previous lemma

c 1 ; c, σ ∼ c, c 1 , σ ✲ + c, σ ′ ✲ ij σ ′′ ∞ ✲ ∞ ✲
First step is just a macro expansion. Second step is the result of syntactic induction: as σ ∈ j+1 .F j+1 ⊆ B ν c 1 ( j .F j ), either there exists a state σ ′ such that σ ′ ∈ j .F j and c 1 , σ → + σ ′ or c 1 , σ → ∞ . The final step results from the recurrence hypothesis. Note that the whole derivation is done in more than j steps, which concludes this case.

⊓ ⊔ Now that we have stated these two lemmas, it remains to conclude the proof. To do it, we consider the set Aux = {i ∈ N | σ ∈ i-1 .F i }. Then, two cases can arise.

1. Either Aux is not empty, and there exists k ∈ Aux.

Then, σ ∈ k-1 .F k and Lemma 5 allows to conclude this case. 2. Or Aux is empty.

Then, ∀j ≥ 1, σ ∈ j .F j . By Lemma 6, we get that either ∃j ≥ 1 such that (σ

∈ j .F j ⇒ c, σ → ∞ ) or ∀j ≥ 1, ∃i j ≥ j -1, c, σ → ij c, σ ′ .
This means that we can always find a derivation as long as we want.

In other words, c, σ → ∞ . This concludes this last case and the proof. ⊓ ⊔

B Correctness

Theorem 9 (Correctness) Let I be a polynomial ideal and c a polynomial program. Then:

γ( c ♯ I) ⊆ B ν c γ(I)
We now prove Theorem 9 by syntactic induction on polynomial programs.

RR n°7627

Proof. Let us apply the hypothesis to νf ♯ . We obtain γ(f ♯ (νf ♯ )) ⊑ f (γ(νf ♯ )). νf ♯ being a fixpoint of f ♯ , we have f ♯ (νf ♯ ) = νf ♯ . Thus, we have γ(νf ♯ ) ⊑ f (γ(νf ♯ )) meaning that γ(νf ♯ ) is a prefixpoint of f . By definition of νf , we conclude that γ(νf ♯ ) ⊑ νf . ⊓ ⊔ We note f the concrete function and f ♯ the abstract function defined by: ⊆ f • γ. Let J 0 be a polynomial ideal. One the one hand, we have:

f • γ(J 0 ) = ( p = 0 γ(I)) ( p = 0 B ν c 1 γ(J 0 ))
On the other hand, we have: This concludes this case.

γ • f ♯ (J 0 ) = γ(<p.
If c ≡ while p = 0 do c 1 : this case is symmetric to the previous one and can be treated in the same way. We do not develop it here. ⊓ ⊔

C Benchmarks

Table 5 presents the results of the Maple implementation of our analysis. Our tests were run on a 2.8 GHz Intel Core 2 Duo sporting 4 Go of DDR3 RAM, on Rodríguez-Carbonell and Kapur's inductive benchmarks [START_REF] Rodríguez | Generating all polynomial invariants in simple loops[END_REF][START_REF] Rodríguez | Automatic generation of polynomial invariants of bounded degree using abstract interpretation[END_REF], and measured to their best and worst results. Our method is systematically better, and on average 2.2 orders of magnitude faster.

A few examples deserve additional comments. We found an higher-order invariant (x = n 3 ) for cohencu starting from the most generic a i -lpp of degree 3 and not restricting ourselves to degree 2 as it is done in Rodríguez-Carbonell and Kapur's work. The same way, we found the higher-order invariant 4r 3 -6r 2 + 3r + 4x -4a = 1 for freire2. In Figure 6, we formally define petter30, a polynomial program that computes the sum of the first n numbers to the power 30 and provides the following invariant of degree 31 at the end of the program.

1.

x := 0; 2.

y := 0; 3.

while y = n do 4.

x := x + y 30 ; 5.

y := y + 1; 6. The knuth program has non-polynomial initial assignments: r = n%d; rp = n%(d -2); q = 4 * (n/(d -2) -n/d); where % denote the modulo operator and / denote the integer division. We introduce two variables n 1 and n 2 to code the integer division and rewrite the assignments into: r = n -n 1 * d; rp = n -n 2 * (d -2); q = 4 * (n 2 -n 1 );. These new variables are necessary to generate the sufficient initial constraints to infer the program invariant.

Finally, Figure 7a and 7b define two programs derived from mannadiv. Their main interest is to introduce non linear polynomial guards in the loop or in the if statements. Proceeding the same way as it is done in the mannadiv example, we infer respectively the polynomial invariants x 2 + 2t + yn = 0 and x 3 + 3t + yn = 0 at the end of the program. These changes do not cause a significative loss of performance of our method since they are respectively generated in 0.005 seconds and 0.008 seconds.

1.

y := n; 2.

x := 0; 3.

t := 0; 4.

while y.(y -1) = 0 do 5.

if t = x then 6.

y := y -1; 7.

t := 0; 8.

x := x + 1; 9. else 10.

y := y -2; 11.

t := t + 1; 12.

(a) mannadiv2.

1.

y := n; 2.

x := 0; 3.

t := 0; 4.

while y > 0 do 5.

if t = x 2 then 6.

y := y -3x -1; 7.

t := 0; 8.

x := x + 1; 9. else 10.

y := y -3; 11.

t := t + 1; 12.

(b) mannadiv3.

  (b) small.

Figure 1 :

 1 Figure 1: Two polynomial programs.

Definition 4 (

 4 Syntax of polynomial programs) p ∈ R[x 1 , . . . , x m ] polynomials V ∋ var ::= x 1 | . . . | x m program variables T ∋ test ::= p ⊲⊳ 0 polynomial guards P ∋ c ::= var := p polynomial assignments | c ; c sequence | if test then c else c conditional structure | while test do c loop structure | skip skip assertion

  )> while p = 0 do c ♯ I = ν(F ♯ c,p,I ) where F ♯ c,p,I = λJ.<p.( c ♯ J), Rem(I, p)> while p = 0 do c ♯ I = ν(F ♯ c,p,I ) where F ♯ c,p,I = λJ.<p.I, Rem( c ♯ J, p)>

6 end 7 Algorithm 1 :

 671 input : a polynomial program c, a natural number d output: a set of polynomials G begin 1 start from g, the most generic a i -lpp of degree d; 2 compute the abstract semantics c ♯ <g>; 3 generate C g,c , the set of constraints equivalent to: c ♯ <g> = <0>; 4 compute S g,c , the set of solutions of C g,c ; 5 define G as the set of all instances of g by elements of S g,c ; Invariant set generation Algorithm 1 generates polynomial invariants of degree d for a program c.

Theorem 5

 5 Let c ∈ P and d ∈ N. Polynomials computed by Algorithm 1 are invariants for c of degree less or equal to d.

Figure 3 :

 3 Figure 3: Performance results for the Maple implementation

  false while while b do c, σ ∼ if b then (c; while b do c) else skip, σ Notation: given σ = (σ1, . . . , σm), we note σ[ [v] ]j the updated state (σ1, . . . , σj-1, v, σj+1, . . . , σm).

Figure 4 :

 4 Figure 4: Small-step operational semantics.

Lemma 3 1 .

 31 For all S ∈ P(R m ), for all σ ∈ R m and polynomial program c ∈ P,σ ∈ B µ c S ⇐ ∃σ f ∈ S, c, σ → + σ fProof. By mathematical induction on the length k of the derivation sequence, we prove the following property for all k ∈ N:σ ∈ B µ c S ⇐ ∃σ f ∈ S, c, σ → k σ fInduction base If k = 0 then the property trivially holds since there is no σ f such that c, σ → 0 σ f Induction step We assume the property for k ≤ m and prove it holds for m + Assume there exists σ f ∈ S such that c, σ → m+1 σ f . If c ≡ skip then c, σ → 1 σ. Thus m = 0 and σ f = σ. As B µ c S = S, the property trivially holds for this case. If c ≡ x j := p then c, σ → 1 σ[v] j for v = p(σ). Thus m = 0 and σ f = σ[v] j . As B µ c S = {σ ∈ R m | σ[p(σ)] j ∈ S}, the property trivially holds for this case. If c ≡ c 1 ; c 2 then c 1 , σ → k1 σ ′ and c 2 , σ ′ → k2 σ f for k 1 and k 2 such that 1 ≤ k i ≤ m and k 1 + k 2 = m. By induction hypothesis, σ ′ ∈ B µ c 2 S and σ ∈ B µ c 1 (B µ c 2 S). As B µ c S = B µ c 1 (B µ c 2 S), the property holds for this case.

  p,S ({}) = F c1,p,S (F n c1,p,S ({})) = ( p ⊲⊳ 0 S) ( p ⊲⊳ 0 B µ c 1 (F n c1,p,S ({}))) Two cases can arise:

f

  = λX.( p = 0 γ(I)) ( p = 0 B ν c 1 X) f ♯ = λJ. < p.( c 1 ♯ (J)), Rem(I, p) >and show that γ • f ♯ .

( c 1 ♯

 1 J 0 ), Rem(I, p)>) = ( γ(p) γ( c 1 ♯ J 0 ) ) γ(Rem(I, p)) = ( γ(p) γ(Rem(I, p)) ) ( γ( c 1 ♯ J 0 ) γ(Rem(I, p)) ) = ( γ(p) γ(Rem(I, p)) ) ( p = 0 γ( c 1 ♯ J 0 ) γ(Rem(I, p)) )The former equality is obtained reasoning the same way as in the if -case, writing R m = p = 0 p = 0 . Now, by induction hypothesis on c 1 , we have γ( c 1 ♯ J 0 ) ⊆ B ν c 1 γ(J 0 ). Reasoning again as in the if -case, we get γ(p) γ(Rem(I, p)) ⊆ γ(p) γ(I). Combining these two inclusions, we get γ • f ♯ .⊆ f • γ, which proves by Lemma 7:γ(νf ♯ ) ⊆ νf γ( c ♯ I) ⊆ B ν c γ(I)

Figure 5 :

 5 Figure 5: Performance results for the Maple implementation

Figure 6 :

 6 Figure 6: petter30, a polynomial program.

Figure 7 :

 7 Figure 7: Two polynomial programs derived from mannadiv.

  Terminating state) A state σ ∈ R m is called terminating for a program c if there exists a state σ f ∈ R m such that c, σ → + σ f . A program c is said to be terminating if each state σ ∈ R m is terminating for c.

	P × R m this relation and → + its transitive closure; the reader can refer to
	Appendix A.1 for details. The operational semantics allows us to define the
	following notions, linked to reachability.
	Definition 5 (
	, ) where ⊆,	and	represent respectively the inclusion, union and intersection of sets.
	RR n°7627

3

Recall that P(R m ) is naturally equipped with a complete lattice structure (P(R m ), ⊆,

RR n°7627

A careful reader will see that our analysis can be set in any F[x1, . . . , xm] where F is a noetherian ring, i.e. a ring satisfiying the ascending chain condition on its ideal set.

The union set of two ideals is not an ideal in general.RR n°7627

Note that this sequence is decreasing if we consider the order induced by ⊑ ♯ .RR n°7627

sawja.inria.fr RR n°7627

If c ≡ while p ⊲⊳ 0 do c 1 Assume p(σ) ⊲⊳ 0 ≡ true then c, σ → 1 c 1 ; c, σ → m σ f . By induction hypothesis, we get σ ∈ B µ c 1 ; c S = B µ c 1 (B µ c S).

Moreover, by the fixpoint definition of the backward semantics of the while-statement, we have:

As σ ∈ p ⊲⊳ 0 B µ c 1 (B µ c S), we have σ ∈ B µ c S.

Assume p(σ) ⊲⊳ 0 ≡ f alse then c, σ → 1 skip, σ → m σ f and m = 1 and σ f = σ. By induction hypothesis, we get σ ∈ B µ skip S = S. Moreover, we have:

The property holds for this last case, which proves that it always holds. ⊓ ⊔ We can now prove the other side of the equivalence.

Lemma 4 For all σ ∈ R m , for all S ∈ P(R m ) and polynomial program c, we have:

Proof. By syntactic induction on polynomial programs. We proceed by case.

If c ≡ skip then we have both B µ c S = S, and for all σ ∈ R m , skip skip, σ → σ which holds, a fortiori, for σ ∈ B µ c S ⊆ R m . Thus we have σ f = σ.

If c ≡ if p ⊲⊳ 0 then c 1 else c 2 then we have:

Now consider σ ∈ B µ c S; two cases arise:

And the small-step semantics provides the first step:

If c ≡ while p ⊲⊳ 0 do c 1 then the backward semantics yields σ ∈ νF c1,p,S where:

Backward concrete while-semantics is obtained by iterating from the top element R m . Thus, we have

and, as σ ∈ B ν c S, then ∀i ∈ N, σ ∈ F i c1,p,S (R m ).

Since B ν c 1 is a -morphism, we have:

) is defined by the union of i + 1 sets, corresponding to the successive unfoldings of the loop. In the rest of the proof, we need to know precisely in which of these i + 1 sets we can found σ. For that matter, we note j .F i the set appearing at line j of F i c1,p,S (R m ). To remove any

Proof. Let I be a polynomial ideal. Note that, by Theorem 1, I is finitely generated. Thus, there exist g 1 , . . . , g s ∈ R[x 1 , . . . , x m ] such that I = <g 1 , . . . , g s >.

If c ≡ skip then c ♯ I = I B ν c γ(I) = γ(I) And thus, this case is trivial.

This case is thus also trivial.

By induction on c 1 , we have:

Now, by induction on c 2 , we have:

As the concrete semantics B ν c is a monotonic function, we conclude this case by applying B ν c 1 to each member of the subset inequality.

The variety of the abstract semantics is:

In order to improve the readability of the proof, we introduce the capital letters A and B (on the right of the previous formula). Now, writing R m as ( p = 0 γ(p)), we have:

The former equality is a direct consequence of the fact that:

To conclude the proof, we prove that:

We first prove inequality [START_REF] Carl | Galois connections and fixed point calculus[END_REF]. By induction hypothesis on c 1 , we have:

Then, intersecting each member of the inclusion by p = 0 , we get:

which proves [START_REF] Carl | Galois connections and fixed point calculus[END_REF].

We now prove inequality [START_REF] Besson | Certified result checking for polyhedral analysis of bytecode programs[END_REF]. Let x be an element of A and u be an element of c 2 ♯ I. We note t = Rem(u, p) and q the quotient associated to this division: u = q.p + t. As x ∈ A, x ∈ γ(p) and so p(x) = 0. We also have x ∈ γ(Rem( c 2 ♯ I, p)). Thus, t(x) = 0, which implies that u(x) = 0. We proved that for all u ∈ c 2 ♯ I, u(x) = 0, which means that x ∈ γ( c 2 ♯ I) and demonstrates that A ⊆ p = 0 γ( c 2 ♯ I). We conclude the proof of inequality (2) thanks to the induction hypothesis on c 2 .

If c ≡ if p = 0 then c 1 else c 2 : this case is symmetric to the previous one and can be treated in the same way. We do not develop it here. ⊑ f • γ

Then we have: γ(νf ♯ ) ⊑ νf


Savitri Jalais
email: savitrijalais@yahoo.com

The river front of Benares: between 'sacred' waters and sewage water

Keywords: Water-architecture, river, sewage

The ghats (steps and landings leading to water bodies) and palaces of Benares, built along the river Ganges between the end of the 17th century and the beginning of the 20th century, appear today as foremost references of monumental water-front constructions. This paper explores the role played by these constructions in establishing a relationship between the Ganges and the city of Benares. While integrating the river to the city they simultaneously protect the city from the river currents raising thus the question: were the palaces of Benares with their ghats and their foundations constructed to play this double role? Furthermore, they are regularly repaired to counter the erosion of the running river water, and the damages caused by leaking drains running along the ghats; sewage flows over them before discharging into the Ganges. We shall present the palaces and their ghats in association to both the running 'sacred' waters of the river Ganges and the sewage water of the city.

INTRODUCTION

The palaces and ghats (steps and landings leading to the water) built along the river Ganges, in the state of Uttar-Pradesh, India (Fig. 1), have consolidated the banks of the river and have protected the city of Benares from river currents and annual floods. Yet, many of these ghats and palaces have, in spite of their grandeur, collapsed and are today in a state of ruin. There are numerous reasons which explain the causes for the damages to these structures, including lack of means to maintain and renovate them. This paper will limit its study to the role of water as a cause for damage: running waters, river water, streams and rivulets, flooded tanks and ponds as well as percolating sewer.

I shall initially present the different palaces and ghats in their historical context followed by the techniques used in their constructions. I shall then proceed to place these structures in their geographical context so as to understand their position in relation to the river and to the drainage system of the city. These structures will be questioned as to how effective they are and if during their construction they take into account the sources of running water which often happens to be the first cause for the crumbling of foundations. We shall discuss how on one hand the structure permits ready access to the river water, considered sacred and purifying for ablution; and on the other hand how the lack of efficient drainage structures pollutes this 'sacred' river. It is frequent to read that the ancient Kashi (the luminous) 1 is the oldest continuously inhabited city. Historically, its date of origin is uncertain and there are doubts regarding the actual position of the ancient site and its correspondence with today's city. However, the city is mentioned in various ancient texts that confirm its importance as a cultural and religious site since 800 B.C. Till today, this city plays an important role as a religious and philosophical place as well as one of the most important pilgrimage sites in India.

The palaces and ghats (Fig. 2), that form today the riverfront of Benares, were built in more recent times. Most were built, in the 18 th and 19 th century, when the city began to be reconstructed. A renewed economic and political stability (after 400 years of Muslim rule) led to the construction of eminent residences and religious complexes. Rich personalities came from all over India and beyond, to build temples, palaces and shelters that would welcome pilgrims. It was prestigious for them to have a presence in the city and monumental constructions were a way to reaffirm their power [START_REF] Freitag | Visualizing cities by modern citizens[END_REF]. They brought with them styles particular to their region and adopted techniques prevalent during the Mughal period in India. These numerous palaces, constructed between the rivulet Assi in the south and the river Varuna in the north, 1 Another name for Benares.

The river front of Benares: between 'sacred' waters and sewage water -Savitri JALAIS 3 / 9 reflect the power not of a unique monarch nor of a single culture but of many contributions and individual wishes of minor kings, rich bankers and patrons from all over India [START_REF] Freitag | Visualizing cities by modern citizens[END_REF]. The city of Benares is closely associated to the Ganges and to the religious character of the river. In the Hindu conception, the water of the Ganges is sacred and purifying. The immersion and ablutions in its waters are an everyday practice for the inhabitants as well as for the pilgrims coming from all over India and beyond. The ghats enable an easy and clean access to the river, and their architecture, as pointed by Julia [START_REF] Hegewald | Water architecture in South Asia: A Study of Types, Development and Meanings[END_REF], is widespread all over India along sacred rivers, lakes, tanks and ponds. However, such a long stretch of ghat construction is particular to Benares. Here, ghats permit an easy access to the city constructed on top of a ridge of firm kankar (concentration of lime) filled clay. This high position is supposed to naturally protect the city from floods, and the ghats further reinforce the banks. This leads us to ask if ghat construction is a tradition or a novelty in its means to protect the city from the river?

TECHNIQUES OF CONSTRUCTION

The foundations of these palaces and ghats are rarely visible as they are covered by the river and extend way below ground surface. One has to depend on different sources to have an idea about the forms and the materials used for their execution. For example, documentation on foundations of hydraulic constructions exist -forts, bridges and sluices, built in the same period as the ghats and palaces of the 18 th and 19 th century. These structures rested on piles of brick masonry, a tradition probably brought to India by the Mughals and used for the foundations of the ghats and palaces of Benares. Another current way to imagine old ghat foundations are by comparing them to those found in other cities. In Vrindavan, where the water of the river has reduced to a considerable length, ghat steps do not descend to the water's edge and foundation piles are exposed , enabling one to have an idea about the dimensions and forms of the ones in Benares (Fig. 3). Medley in 1873 gives a brief description of foundations built along rivers [START_REF] Medley | India and Indian engineering: three lectures delivered at the Royal Engineer Institute[END_REF]. According to him, wooden piles were rarely used as timber was scarce and was prone to rot. Instead cylinders of brick masonry were used, three to twelve feet in diameter, sunk to firm stratum and safe from river erosions. 'A sufficient number of wells are designed to carry the super-incumbent weight whether it be a house or the pier of a bridge, and the whole series being sunk to the required level, and as close together as possible; the tops of the wells are arched over, the arches are all connected together by slabs of stones or other arches, and on this artificial platform the superstructure is raised' (Medley, 1873, p.15) (Fig. 4). Today, many of the new ghats being constructed or the old ones getting repaired use five meters high RCC (reinforced cement concrete) piles placed every two meters. To further protect these piles from the water currents, huge boulders are heaped up in front. On the other side, a mixture of sand, broken stone and cement cover the surface of the bank on which stone steps are arranged.

Stone steps or ghat like structures are common today for the more important ghats (like Assi ghat where stone is used for each step -Fig. 8), however less known banks are often reduced to just a sheer expanse of steep retaining walls, now and then broken up into terraces. This kind of intervention is implemented to reduce expenses while at the same time insuring the protection of the ghats. Instead of stone, brick (much cheaper in cost and execution) is used on the surface.

A thorough survey on site will be needed to study more closely the structure of the ghats and palaces in their context. Primarily, it will be important to calculate how effective the new structures are and compare them to the old ones. Secondly, their permeability will be questioned in relation to the river and to the drainage and sewerage systems, especially in relation to the overflow of sewage.

DRAINAGE AND SEWERAGE SYSTEM IN RELATION TO THE GEOGRAPHICAL CONTEXT

According to Singh, « just as the banks would most probably have been protected in the past thanks to the forest that covered this site, so today the stability of the bank is maintained by the construction of ghats and palaces » [START_REF] Singh R | Banaras: a study in Urban Geography[END_REF]. Based on the map of Prinsep, Dr. R.L.Singh has drawn in his book a figure which illustrates the initial physiographic conditions of Benares. Along the river Ganges a high ridge can be seen, extending almost continuously from one end of the city to the other interrupted only at Dasaswamedh ghat by the Godaulia nala2 . This high ridge, made of clay and kankar (lime concentration) acts as a solid natural barrier protecting the city from the river. The palaces and ghats of Benares have been constructed on this high ridge further consolidating the banks (Fig. 5). They form the extremity of the city and are mainly designed in relation to the river water and are thus very different from the rest of the buildings found in the city. This river front seems to be constructed independent to the city that spreads out behind. In Prinsep's map of 1828 (Fig. 6), the level of land on the other side of the ridge slopes down slightly and a series of ponds and tanks are found all along the ridge. Initially, these tanks were supposed to collect the drainage and direct it either through the Varuna river or through the Godaulia nala into the river Ganges. However, with the densification of the city, most of these ponds and nalas have been filled up. Till what extent were the construction of ghats and palaces linked to the infrastructure of the city? Actually, rich personalities were ready to pay large amounts for the development of religious structures in the city: ghats, temples, dharamshalas (shelters for pilgrims). To a certain extent, public welfare too was financed by the patrons of the city as an act of piety. However, the city spread in an unplanned way and there lacked a powerful coordinating body that would effectively work on the management of large infrastructures. A committee did form for a very short period. It functioned from 1826-1829 and began various works for the development of the city. Prinsep, who was its secretary, pointed out that « while resident pensioned noblemen and disinherited princes were embellishing the City in massive stone above ground the members of the committee would content to labour in humble brick underground » (quoted in Swami Medhasananda, 2002, p.435). Before the beginning of the 18th century Varanasi had an extensive system of underground drains meant primarily for carrying rain-water. These were large drains unsuitable for the flow of sewage as they were rectangular in shape with irregular gradients. Made of brick and rough stone work (from 1 to 6 feet wide and from 1 to 9 feet deep.) they ran at varying levels down the centre of the paved lanes, connected with courtyards of houses. They later played a role in the laying and development of a new sewer at their old site. Actually, the committee that worked for the improvement of the city in 1826 designed one main sewer, carrying the entire sewage of the city. It was built running down the stream and dropping the sewage into the Ganges near Rajghat [START_REF] Singh R | Banaras: a study in Urban Geography[END_REF].

Around 1867 a municipal Board was instituted that introduced improved sewerage and drainage facilities. However, an entire sewerage system was introduced in the city only in 1891 and completed by 1917. This must have been the time when most of the tanks and nalas were filled up, either for construction of buildings or for establishing new roads (eg. The Godaulia nala was transformed into a sewer with the Dasaswamedh road built over it).

With time this sewage system installed became inadequate with the quickly expanding city. Furthermore, numerous leaks in the pipeline led to overflow of sewage directly into the Ganges at several places (Fig. 7). There are several records of palatial houses collapsing because of these leakages. Already in 1955, Singh mentions that « the reconstruction and improvement of the ghats as also the improvement of the drainage system are interrelated problems and need to be tackled at the same time » (Singh, 1955, p.44).

In 1971, to prevent the pollution of the river at the important ghats, a new sewerage system was added. This system, constructed on the bank of the river, intercepts the sewage discharges to the river and is called the "Ghat intercepting sewer". The sewage discharge comes from a number of old drains from the ghat portion of the town and all the sewer that cannot be drained into the main sewer (Report, 1986). on. Therefore, during power cuts, which occur at regular intervals during the day, these pumps cease to function. The sewage then flows directly into the river over the ghats. In places where the river is used for domestic or ritual purposes there are some arrangements done to shift this same sewage, through pipes and manholes, a little distant off. But, this does not prevent the pollution of the 'sacred' river by the sewage water.

CONCLUSION

In a city of over 1.2 million habitants, the pollution of the river presents a health hazard specially to those who bath in it and drink its waters Many organisations have sprung up within the city to try and find a solution to the problems linked to the pollution of the Ganges. There is a contradiction in the fact that 'Ganga water' supposed to purify should have 'a fecal coliform count, in the religious bathing areas of the ghat, 10,000-100,000 times higher than acceptable level' (Kirchner, 1997). This short presentation tries to associate the lack of adequate sewage facilities to the architecture of the river front. It invites to study documents elaborated by the different bodies responsible for the maintenance of the ghats, the drains, the sewer, and the water pollution of the Ganges and question the existing links between these different bodies.

8th 9 Figure 1 :

 91 Figure 1: Benares is built on the river Ganges, in the state of Uttar-Pradesh, India

Figure 2 :

 2 Figure 2: View of the ghats and palaces

9 Figure 3 :

 93 Figure 3: Masonry wells as foundation piles in Vrindavan

Figure 4 :

 4 Figure 4: Foundations on piles of brick masonry called wells (example of a sluice in central India).

Figure 5 :

 5 Figure 5: Diagrammatic section on the river bed in Benares, not to scale (drawn by the author)

8th 9 Figure 6 :

 96 Figure 6: Map of prinsep, 1828 Figure 7: Overflow of sewage causing destruction of palatial houses

Figure 8 :

 8 Figure 8: Construction of Assi Ghat (picture by Pierre Toutain in Bénarès, BNP Paris, 1985)

Figure 9 :

 9 Figure 9: Plan of the Ghat intercepting sewer Figure 10: Pumping station at Lalita ghatToday, the scene of the ghats are much denatured by the presence of huge cylindrical often light pink coloured sewer pumping stations constructed along the entire river front (Figs. 9 and 10).. These structures are supposed to pump out the sewer drained towards the ghats, and take it towards a treatment plant. Six major drains, which pass through densely populated areas of the city before discharging into the river, are tapped and pumped at the 5 pumping stations. The problem is that these pumps work on high electrical means which the city cannot afford to invest

The river front of Benares: between 'sacred' waters and sewage water -Savitri JALAIS

Nala : it can signify a big drain, a gutter, a rivulet or a watercourse.