Clotilde Erard

Jérome Ricciardi

Alain Giorgetti

Towards Random and Enumerative Testing for OCaml and WhyML Properties

Keywords: property-based testing, random testing, enumerative testing, deductive verication

come

Introduction

By proving that a given program respects a given functional specication, once for all its possible inputs, deductive verication, aka program proof, provides a high level of condence in software correctness. However, many obstacles limit the spread of deductive verication and its practice by development and validation engineers, despite the existence of numerous deductive verication tools.

The rst obstacle is the formalization of specications. Their writing has become easier thanks to a syntactic entity of formal assertion available in some programming languages and to behavioral interface specication languages, aka contract languages, that are close to programming languages and are integrated in code as formal comments, named annotations. Examples of contract languages are JML for Java [START_REF] Leavens | JML: A notation for detailed design[END_REF], ACSL for C [START_REF] Baudin | ACSL: ANSI/ISO C Specication Language 5[END_REF] and Spec# for C# [START_REF] Barnett | The spec# programming system: An overview[END_REF]. Deductive verication tools such as KeY [5] for Java/JML, the WP plugin [START_REF] Correnson | Qed. Computing what remains to be proved[END_REF] of Frama-C for C/ACSL or Boogie [START_REF]The Boogie intermediate verication language[END_REF] for Spec#/C# then reduce annotated code to logical formulas, named verication conditions, whose validity entails conformance between the code and its specication.

Unfortunately, the complexity of main-stream programming languages often leads to verication conditions that are too dicult to be automatically proved by deductive verication tools. A good strategy is to write specication and programs in the language of a tool dedicated to deductive verication, such as Why3 [START_REF] Bobot | The Why3 Platform[END_REF], which optimizes the interface with automated provers.

A remaining issue is that deductive verication tools often do not provide enough feedback to understand why a proof fails. A recent work has shown how automated test generation can provide a better understanding of the origin of proof failures, by classifying them as prover weakness, wrong specication or incomplete specication [START_REF] Petiot | How testing helps to diagnose proof failures[END_REF]. Why3 integrates a prover-based counterexample generator [START_REF] Hauzar | Counterexamples from proof failures in SPARK[END_REF], but this feature suers from the limitations of the external provers exploited to nd these counterexamples [START_REF] Kosmatov | Static versus dynamic verication in Why3, Frama-C and SPARK[END_REF].

Following the principles of property-based testing, we suggest to supplement deductive verication tools, such as Why3, with the ability to test the properties to be veried. We present design principles and illustrate them with a prototype, named AutoCheck, to test properties written in WhyML, the specication and programming language of Why3. AutoCheck aims at the integration of the complementary techniques of random and enumerative test data generation. AutoCheck is not yet complete enough for industrial applications, but it can already be used and extended by OCaml and WhyML developers. It is presented here as a proof-of-concept for the following design choices, which are as many contributions:

1. AutoCheck includes a library of enumeration programs in WhyML, named ENUM, which are certied by formal proofs with Why3.

2. AutoCheck integrates the mature third-party random testing tool QCheck [START_REF]QuickCheck inspired property-based testing for OCaml[END_REF] for OCaml.

3. AutoCheck completes QCheck with random testing for WhyML properties and enumerative testing for WhyML and OCaml properties.

This implementation of random and enumerative testing for WhyML exploits

Why3's extraction mechanism from WhyML to OCaml and an implementation of random and enumerative testing for OCaml. This shallow approach by extraction greatly reduces the amount of code to develop.

The paper is organized as follows. Section 2 introduces some background about property-based testing and the tools involved in AutoCheck design, presented in Sect. [START_REF] Baudin | ACSL: ANSI/ISO C Specication Language 5[END_REF]. Section 3 presents our library of certied enumeration programs and the principles of their certication by formal proofs with Why3. Section 5 is a tutorial on random testing for WhyML properties. Section 6 presents our implementation of enumerative testing for OCaml and WhyML. Section 7 is dedicated to concluding remarks.

Background

This section shortly presents OCaml, the Why3 platform and its extraction mechanism (Sect. 2.1), the principles of property-based testing and the notion of property in this context (Sect. 2.2), some background on existing tools for random and enumerative testing (Sect. 2.3) and a discussion about various possible origins of properties for property-based testing (Sect. 2.4).

OCaml and Why3

OCaml is a programming language developed and distributed by INRIA since 1996 [START_REF]What is OCaml?[END_REF]. The powerful type system, as well as the automated memory management (incremental garbage collector) make OCaml a very safe language. It comes with a compiler producing native code for many architectures, and a compiler producing bytecode, for increased portability.

Why3 is a platform for deductive program verication. Programs for Why3 are written in the language WhyML, a verication-oriented dialect of ML with some functional features, such as polymorphic algebraic types, but also imperative features, such as loops or records with mutable elds.

WhyML oers usual non-mutable types such as unit, bool, int, or the polymorphic type list `a, where `a is a type variable that can be replaced by any type. WhyML also oer mutable types such as array 'a. It is possible to change the value of a variable if its type is mutable. The value of a variable with a nonmutable type cannot be changed, but it is possible to declare a reference on a non-mutable type, with the keyword ref, and to access its value with the operator !. Some syntactic sugar is provided to lighten the notation a documentation on this can be found in Why3's manual [52, section 7.4.3].

The functional behavior of WhyML programs can be specied with formal annotations, globally called contracts: preconditions, postconditions, invariants and loop variants, assertions, etc., in a rst-order logic with polymorphic types.

Why3's standard library denes theories or data structures for common types such as integers, lists or arrays. Why3 reduces programs and specications to logical verication conditions whose satisability entails that the programs meet their specications. Then, automated provers (e.g., SMT solvers) or proof assistants (e.g., Isabelle [10] or Coq [START_REF]The Coq proof assistant[END_REF]) can be used to prove these logical statements.

Why3 also provides a driver-based automated extraction mechanism. The driver maps WhyML symbols to the syntax of the target language. A user can write WhyML programs directly and get correct-by-construction OCaml [START_REF] Pereira | Tools and Techniques for the Verication of Modular Stateful Code[END_REF] programs using the OCaml driver provided by Why3. Why3 also accepts custom extraction drivers. Thus, the extraction can be adapted to dierent languages, as is the case for the C [START_REF] Rieu-Helft | Un mécanisme d'extraction vers C pour Why3[END_REF] or Rust [START_REF] Fitingho | Extraction of Rust Code from the Why3 Verication Platform[END_REF] languages. or even assess external eects (matches the output of a trusted external program). [START_REF] Nelson | The design and use of QuickCheck[END_REF].

Property-based testing

Property-based testing (PBT, for short) consists in identifying and testing a set of properties that some functions should satisfy. Beyond the basic case of function contracts, that are properties about one call of one function, properties addressed here are relational properties which can concern several functions and/or several calls of the same function [START_REF] Blatter | Static and dynamic verication of relational properties on self-composed C code[END_REF]. Some tests of relational properties are presented in Sect. 5. Temporal properties, written in a temporal logic such as LTL, CTL or µ-calculus, are out of the scope of the present work.

Along the line of many property-based testing tools described in Sect. 2.3, we assume that each property to be tested comes under the form of an executable function returning a Boolean value providing the test oracle (true if the test passes, false if it fails). Hereinafter this function is often called an executable property.

We shall see in Sect. 2.4 how properties could be derived from functional specications. The task of identifying the properties to be tested can be dicult, especially for programmers who have no background in formal program verication. Property-based testing can allow these programmers to become familiar with formal methods, while increasing their level of code understanding, since reasoning about code properties forces us to reason at higher levels of abstraction than we do with traditional unit tests. For more advanced users in formal verication, property-based testing can be an excellent complement during the formal proof process, allowing the discovery of incomplete or erroneous understanding of logical conjectures or specications. Before investing time in interactively proving a non-trivial lemma or theorem, it is wise to test it.

Random and enumerative testing tools

Our goal is to adapt to OCaml and Why3 the two most basic and oldest techniques of PBT, which are random and enumerative testing. The integration of more recent PBT approaches, such as fuzzing [START_REF] Padhye | JQF: Coverage-guided property-based testing in Java[END_REF], may be studied later. Below we list some random and enumerative testing tools and we note the complementarity between the two approaches.

Random testing. Random testing consists of the automatic generation of random test cases. The ancestor of property-based random testing is the QuickCheck tool [11], originally written for the Haskell language. It has been adapted to more than thirty languages (see, e.g., fast-check for JavaScript [START_REF]Property-based testing framework for JavaScript[END_REF], jetCheck for Java [START_REF]Property-based testing library for Java 8+[END_REF], PropEr for ERlang [START_REF]PROPerty-based testing tool for ERlang[END_REF], QuickChick for Coq [START_REF]Randomized property-based testing plugin for Coq[END_REF] and theft for C [START_REF]Theft: Property-based testing for C[END_REF]).

There are several random testing tools for OCaml, e.g., the QuickCheck module from JaneStreet's core_kernel framework [START_REF]Module core_kernel.quickcheck[END_REF], Kaputt [START_REF] Reis | Kaputt[END_REF], Crowbar [START_REF] Dolan | Crowbar -Git[END_REF] or QCheck [START_REF]QuickCheck inspired property-based testing for OCaml[END_REF]. Among them, we choose to embed QCheck in our prototype. Used to test OCaml functions [START_REF] Midtgaard | QuickChecking static analysis properties[END_REF], QCheck provides many useful combinators to generate dierent types of data, and also allows users to write their own generators, especially for recursive types, algebraic types or tuples. QCheck also provides the shrinking function, which reduces the size of the counterexample provided in case of test failure. For example, if the tested property is the existence of a given number in a list, it should return a list of length 1 containing only this number.

In addition, QCheck is used in several OCaml teaching courses [START_REF] Midtgaard | Functional programming and property-based testing[END_REF][START_REF] Miné | QuickCheck de bibliothèques d'analyse statique en OCaml[END_REF][START_REF] Naves | Programmation fonctionnelle[END_REF].

Enumerative testing. Enumerative testing, also known as bounded exhaustive testing (BET, for short), is used in a variety of property-based testing tools.

It consists of generating and testing all possible inputs at a size limit. It has rst been used to check properties of functional languages, as exemplied by SmallCheck in Haskell [START_REF] Runciman | SmallCheck and Lazy SmallCheck -automatic exhaustive testing for small values[END_REF]. Then, it has been adapted to several proof assistants, e.g., to Isabelle in Quickcheck [START_REF] Bulwahn | The new Quickcheck for Isabelle -random, exhaustive and symbolic testing under one roof[END_REF] and to Coq, in an extension of QuickChick named CUT (Coq Unit Testing) [START_REF] Dubois | Tests and proofs for enumerative combinatorics[END_REF]. In a former work we have initiated a BET tool for WhyML [START_REF] Erard | Bounded exhaustive testing with certied and optimized data enumeration programs[END_REF].

Complementarity. The complementarity of random and enumerative testing becomes clear after listing some advantages and drawbacks of both approaches. Indeed, while an enumerative test is useful for small data sizes [START_REF] Duregård | Feat: functional enumeration of algebraic types[END_REF], the number of test cases often increases exponentially with the size limit, meaning that the test becomes too slow, perhaps impossible, beyond a relatively small input size. Random testing can be an alternative to check data with large size. Unfortunately, random testing does not support existential properties: the random testing would rarely give useful information about an existential property: often there is a unique witness and it is most unlikely to be selected at random [START_REF] Reich | Advances in Lazy SmallCheck[END_REF].

Enumerative testing, in contrast, is more likely to nd this witness or prove its absence below some size.

Where can properties come from?

Most PBT tools, starting with the pioneer QuickCheck for Haskell, generate tests from user-provided properties, i.e., properties assumed to be handwritten by the user. Can we further assist the user, with methods and tools that would automatically generate executable properties from formal specications? We briey explore this question in the context of the OCaml and WhyML languages.

The answer depends on the language: In a programming language like OCaml, a property can only be specied as a function returning a Boolean value, because the language supports no syntactic entity for logical formulas. In a logical framework such as Coq, an executable property could also be derived from a conjecture a not-yet-proved lemma or theorem in order to detect errors in it before attempting to prove it. In a language such as WhyML, for logical formulas, programs and formal program specications, a property can again be a function returning a Boolean value or be derived from a conjecture, but it might also be derived from programs and their formal specications.

Whatever the possible origin of a property in a given language, to be tested it has to be turned into an executable function returning a Boolean value. This implementation can be arbitrarily hard or impossible, since it is nothing less than providing a decision procedure for the problem expressed by the property.

It is therefore restricted to the limits of decidability.

In the deductive program verication method implemented in Why3, the program and its formal specication are transformed into verication conditions (VC, for short) by a verication condition generator (VCGEN, for short). Then external automated provers are called separately on each VC, to try to prove it.

Because these automated proof attempts can fail or take much time, it can be useful to supplement them with PBT on these VC.

For the sake of simplicity we hereafter say that the properties under test are user-provided, even if they may be produced mechanically by some executable property generator, as detailed here. The design of such a tool is left as future work. For now, AutoCheck helps nd errors in user-provided properties, thus playing a role similar to that of an automated prover in the deductive method.

3 Library of certied enumeration programs Some enumerative testing tools implement techniques such as constraint solving or local choice with backtracking, either to enumerate data or to derive eective generators from data denitions (see [START_REF] Dubois | Tests and proofs for custom data generators[END_REF]Sect. 7] for references). However, these techniques may fail or provide too slow enumerations. For eciency and generality, we consider enumerative tests with custom enumeration programs (sometimes hereafter called generators), which are dierent enumeration programs handwritten for each family of data of interest.

Condence in enumerative testing is increased if its enumeration programs are certied, ideally with formal proofs of their properties. Genestier et al. [START_REF] Genestier | Sequential generation of structured arrays and its deductive verication[END_REF] developed a rst version of a library of enumeration programs in the C language, named ENUM, whose properties were formally specied with ACSL clauses and proved with the Frama-C plugin WP for deductive verication [START_REF] Correnson | Qed. Computing what remains to be proved[END_REF]. A large fragment of this library has been adapted in WhyML and certied with Why3 [START_REF] Erard | Bounded exhaustive testing with certied and optimized data enumeration programs[END_REF].

ENUM is freely distributed at https://github.com/alaingiorgetti/enum. Its programs implement algorithms that enumerate combinatorial structures [START_REF] Arndt | Matters Computational -Ideas, Algorithms, Source Code[END_REF] and have various applications in combinatorics. This section details the principles and contents of the library ENUM. All enumeration programs implement the same interface and share the same specication, both described in Sect. 3.1. As an illustrative example, the implementation and certication of a generator of permutations are presented in Sect. 3.2. Section 3.3 presents a simple way to dene a generator, by ltering the output of another generator. The certied enumeration programs distributed to date are described in Sect. 3.4. The integration of ENUM in AutoCheck is detailed in Sect. 6.2.

Generic interface and contract of enumeration programs

Since enumeration is a particular form of iteration, the enumeration programs in ENUM are adaptations of the modular iterators dened by Filliâtre and Pereira [START_REF] Filliâtre | Itérer avec conance[END_REF][START_REF] Filliâtre | A modular way to reason about iteration[END_REF]. They modify a state, called a cursor, whose type is type cursor = { current: array int; mutable new: bool; } in WhyML. The eld current only stores the last data generated so far. For simplicity, it is here a mutable array of integers, but the approach could be extended to other datatypes. The Boolean ag new is set to false if and only if the data stored in the current eld has already been exploited, for instance to test a property. Each generator is expected to satisfy the following behavioral properties.

Soundness is the property that each generated data satises the characteristics (or data invariant) of its family, such as being a duplicate-free or a sorted array. Completeness is the property that the program produces all existing data with a given length, without omitting any of them. Generally, proving completeness is more challenging than proving soundness. Therefore, we limit ourselves to algorithms enumerating data in a predened strict total order, hereafter denoted by ≺, and we adopt two strategies. The rst strategy is to specify completeness as the conjunction of the following three properties: the property min that the rst generated data is the smallest one, the property max that the last generated data is the largest one, and the incrementality property that each data a 2 generated from data a 1 is the smallest data strictly greater than a 1 . In other words, no sound data a 3 is such that a 1 ≺ a 3 ≺ a 2 . When proving completeness seems too dicult, the second strategy is to address the less challenging property named progress that each generated data is strictly greater than the former generated data. Since we assume that there are nitely many data with each length, progress entails termination of enumeration.

Listing 1.1 shows a formalization of these properties in WhyML, as contracts (pre-and postconditions) for the enumeration functions. The precondition on Line 2 species that the length n of data should be a natural number. Most of the properties are formalized by postconditions guarded by a condition on the value of the cursor eld new. Indeed the value of this Boolean ag should be initialized to true if and only if the set to be enumerated is not empty, and set to false as soon as the set of data remaining to be enumerated becomes empty. This informal specication of the cursor eld new could also be formalized as postconditions for functions create_cursor and next. Since proving this additional contract can be hard, we defer these specications and proofs for future work.

We assume that a predicate predicate sound (c: cursor) encapsulates the data invariant. Then, a generator is sound if the rst generated data satises this predicate (postcondition on Line 3) and if the output of the next function satises this predicate (postcondition on Line 8) whenever its input does (precondition on Line 7). The progress property is formalized on Line 9, with a predicate lt formalizing the strict total order ≺. (The expressions (old e) and e in a function postcondition respectively denote the values of the expression e before and after the function call.) The properties min, incrementality and max (entailing the completeness property) are respectively formalized on Lines 4, 10 and 11, with predicates min, inc and max respectively formalizing minimality, incrementality and maximality of the restriction of the order ≺ to data satisfying the data invariant sound.

The library ENUM provides formal denitions (in WhyML) of these predicates min, inc and max for any data invariant, when the order ≺ is the lexicographic order induced on arrays of integers by the standard order < on integers.

Thus, the designer of a program enumerating a new family of integer arrays in lexicographic order can re-use these denitions. She just has to implement the enumeration functions and perform their deductive verication, as detailed on an example in Sect. 3.2.

The contracts of the enumeration functions are proved by a combination of the following two deductive verication techniques: Auto-active verication [START_REF] Leino | Usable auto-active verication[END_REF] consists in providing additional specications, such as variants (for termination), invariants, assertions and lemmas (for partial correctness), before running an automated prover. Interactive verication consists in reducing the proof goal step by step, by applying rules named tactics in Coq and transformations in Why3.

Certied enumeration of permutations

This section presents an implementation and a deductive verication of enumeration functions for permutations on the set [0..n -1] of rst n natural numbers. We encode such a permutation p by the integer array a of its images. It is the array of length a.length = n such that a[i] = p(i) for 0 ≤ i < n.

for i = 0 to n-1 do invariant { 0 ≤ i ≤ n } invariant { is_id_sub p 0 i } p[i] ← i done; { current = p; new = true } Listing 1.2.
Initialization function for a generator of permutations.

The function rst creates an array initialized to 0 (Line 6), then sets each array value to its index (Line 10). The second invariant (Line 9) asserts that at each loop iteration the array is the identity up to the current index. The postconditions ensure the soundness property (Line 3) and the minimality property (Line This function calls two auxiliary functions swap and reverse not reproduced here. The function swap comes from Why3's standard library. The statement (swap a i j) swaps the elements of the array a at the indices i and j. The function reverse is such that (reverse a l u) reverses the subarray a[l..u -1] of the array a.

In order to lighten the code, the variables p and n respectively represent the current permutation and its size. If this size is 0 or 1, the current permutation is the last permutation (c.new ← false). Otherwise, the program proceeds by revising the sux of the array p, as detailed in the following execution example. Let p be the integer array i 0 1 2 3 4 5 p[i] 4 1 2 5 3 0 storing the values of a permutation on [0..5], also noted p (p[i] = p(i) for i = 0, . . . , 5). The program transforms the array p in place, in order to turn it into the smallest array p that is strictly greater than p (according to the lexicographic order ≺) and represents a permutation p . The rst step of the program (lines 14-20) looks for the revision index r such that p and p have the largest common prex p[0..r -1] = p [0..r -1]. When p is a permutation, this index is the largest index i such that p[i] is less than p[i + 1]. In our example of permutation p, the revision index is r = 2. The sux is the subarray p[r..n -1], from the revision index to the end of the array. The second step of the program (lines [START_REF] Giorgetti | Preuve de programmes d'énumération avec Why3[END_REF][START_REF] Giorgetti | Combinatoire formelle avec why3 et coq[END_REF][START_REF] Hauzar | Counterexamples from proof failures in SPARK[END_REF][START_REF] Herdt | Verifying instruction set simulators using coverage-guided fuzzing( * )[END_REF][START_REF]Property-based testing library for Java 8+[END_REF][START_REF] Knuth | The Art of Computer Programming[END_REF][START_REF] Kosmatov | Static versus dynamic verication in Why3, Frama-C and SPARK[END_REF] determines the new value of p[r], such that the array p is greater than p, is as small as possible and represents a permutation. This new value of p[r] is the smallest value p[j] greater than p[r] and present in the subarray p[r+1..n-1] after the revision index. In our example, it is the value p[4] = 3, for j = 4. The third step (line 31) exchanges the values of p[r] and p[j], thanks to the function swap. We obtain then the array p 1 = 4 1 3 5 2 0 . The fourth step (line 32) computes the smallest possible subarray p [r + 1..n -1]. For p to be a permutation, this subarray must be the subarray p 1 [r + 1..n -1] sorted in ascending order. Since this subarray p 1 [r + 1..n -1] is sorted in descending order, it is sucient to invert it with the function reverse, which produces the array p = 4 1 3 0 2 5 . If a revision index was not found during the rst step, then r is -1 and p is the last permutation, which is indicated by assigning the value false to the new

Random testing for Why3

This section is a tutorial on random testing for WhyML properties with Au-toCheck. The pre-release presented in this paper provides random generators for WhyML built-in types (unit, bool and Cartesian products) and some types from Why3's standard library ((option 'a), (list 'a) and (array 'a), for any type variable 'a). The tutorial presents examples of random tests for each type, in increasing order of complexity. The tested properties are either lemmas in Why3's standard library or relational properties between functions dened in that library. In order to eliminate any risk of confusion between a function under test returning a Boolean value and an executable property, the name of all the user-dened executable properties presented below is suxed by _prop.

Basic types and Cartesian products

Example for the unit type. The most elementary type in WhyML (and OCaml) is unit. Its unique inhabitant is (). ---Failure ----------------------------------------------Test is_unit_prop failed (0 shrink steps):

() ---------------------------------------------------------The test fails, as expected, and prints as counterexample the inhabitant () of type unit.

Random tests for two Boolean functions. Let us now consider the type bool for Booleans. The Boolean functions andb, orb, notb, xorb and implb, respectively for conjunction, disjunction, negation, exclusive disjunction and implication on Booleans are dened in Why3's standard library 1 . (This is not a language con- straint, but, for clarity, the name of each Boolean function used or dened here ends with a 'b', when it is not intended to be an executable property. Examples of random tests with integers. Now let us consider the WhyML type int for integers and its theory in Why3's standard library. Since WhyML integers represent unlimited mathematical integers, they are usually extracted to the arbitrary-precision integers of Zarith OCaml library [START_REF]The zarith library[END_REF]. However QCheck for OCaml does not provide any support for arbitrary-precision integers, and it is tricky to extend it to Zarith, because a choice must be made between the types Zarith.t of arbitrary-precision integers and int of limited-precision integers for each use of integers in this third-party code. Therefore, we have chosen to extract WhyML integers to OCaml regular integers. Of course, this semantical change may lead to contradictions between test and proof results.

Properties with integers can only be safely tested under the hypothesis that there will be no arithmetic overow.

AutoCheck promotes to WhyML the three random generators of integers dened in QCheck: a random generator int of OCaml integers, a generator int_range of random values in some interval [a..b], and a generator int_bound of random values in some interval [0..n]. The following example shows how using a generator of limited integers increases the chances of nding a counterexample. Consider lemma Abs_pos: ∀ x:int. abs x ≥ 0 about the abs function from Why3's standard library. The lemma claims that the absolute value of a number is non-negative. Let us test a mutation of this property, where the large order ≥ is replaced by the strict order >. The corresponding lemma is on Line 1 in Listing 1.9. This false property is implemented as shown on Line 3 and tested with two dierent random generators as shown on Lines 5-6 and 8-9 in Listing 1.9.

Option type

The option type in WhyML is dened in Why3's standard library by a module reproduced in Listing 1.11. In the type denition, 'a is a type variable, which can be replaced by any type expression. Thus, we consider here the rst example of random testing with a polymorphic type. In WhyML a denition starting with let predicate simultaneously denes a logical predicate (for specications) and an executable property (for computations).

Thus, the function is_none implements (for free) the (false) property that the only inhabitant of type (option 'a) is None.

let is_none_test = QCheck_runner.run_tests ( Test.make QCheck.(option QCheck.int) is_none)

Listing 1.12. Example of test for option type.

The listing 1.12 shows how to randomly test this property. For the option type, AutoCheck promotes to WhyML the random generator (option _) dened in QCheck. Inspection of its code reveals that it chooses the constructor None in 15% of the cases. When it chooses the constructor Some, it uses the generator provided as parameter to derive data of type 'a. In this example, it uses a random generator of integers named Qcheck.int.

---Failure --------------------------------------------------------------------Test is_none failed (63 shrink steps): Some (0)

QCheck always nds the counterexample Some (0). Any term of the form Some (_) would be a counterexample for the wrong property claiming that the type option is only inhabited by None, but here shrinking is in action and the tool chooses the integer 0 instead of any integer.

Polymorphic lists

The basic theory of polymorphic lists in Why3's standard library contains the The test fails after reducing the counterexample to a list of length 1:

---Failure ----------------------------------------------Test is_nil failed (64 shrink steps):

[true] --------------------------------------------------------- After execution, the test fails by returning a list of length 1 containing an odd integer.

Polymorphic arrays

The theory of polymorphic arrays in Why3's standard library species as follows a function make creating an array of length n whose elements are all initialized with value v: The rst one accepts as rst parameter any random generator of integers for the length of the generated arrays, whereas the second uses an implicit random generator of natural numbers to choose this length.

Enumerative testing

The rst pre-release of AutoCheck presented in this paper oers enumerative testing for the OCaml types unit, bool, int, ('a option), (int array) and (int list), and for the corresponding WhyML types unit, bool, int, (option 'a), (array int) and (list int), where 'a is a type variable. Subsequent releases will moreover cover Cartesian products, polymorphic lists and arrays and user-dened types, which require a more substantial implementation eort. Section 6.1 presents a basic example of an enumerative test for WhyML properties. Section 6.2 details the integration in AutoCheck of the certied enumeration programs presented in Sect. 3. We can notice that all these tests of this property take less than one second.

However, a precise interval and luck are required for the random test to nd a counterexample, whereas the enumerative test always nds a counterexample, even with a large interval of data. Thus, this example illustrates an advantage of enumerative testing over random testing.

This example and the one in Listing 1.9 make it clear that the syntaxes of random and enumerative tests have been made so similar that it is elementary to turn a random test into an enumerative one, when a generator is available for it. This integration of random and enumerative testing should be reinforced on two points: instead of being dened in two modules presenting a similar interface, both modules could clone a single module dening a more abstract common signature. This would make it possible to mix random and enumerative generation, e.g. have an array generator that uses an enumerator for its length, up to a xed size, and a random generator for the array elements.

Integration of certied enumeration programs

Enumerating integer arrays is realistic and useful when their length and range of values are not too large. It is typically the case when arrays represent combinatorial objects such as permutations. An exhaustive testing of some array property, up to a given upper bound for array length, can also be considered as a partial proof (by enumeration) of that property. In Sect. 3 we have presented several eective programs enumerating arrays satisfying given invariants, such as being sorted or duplicate-free, and their certication with Why3. This section presents their integration in AutoCheck.

Illustrative example. The function b_permut allows us to dene an executable property for (P 1 ), as follows:

let inverse_in_place_permut_prop (a: array int) : bool = let newa = copy a in inverse_in_place newa; b_permut newa Here, the latter is a generator of permutations from ENUM library, automatically extracted with Why3 from a certied generator of permutations written in WhyML.

Each enumerative test is executed by the OCaml function SCheck_runner.run_tests, which enumerates all data and checks the same property for each data, thanks to the provided test oracle. Moreover, the execution counts the number of passing data before failure. So, the output is either a counterexample or the number of passed tests. For the present example the output is:

Test inverse_in_place_permut_prop succeeds (ran 720 tests)

Property (P 2 ) is checked similarly.

Enumerative testing is suitable for arrays containing integers in a small interval, as it is the case for permutations here. For larger integer ranges, random generation is preferable.

Conclusion

In this work, we laid foundations for random and enumerative data generation to test properties expressed in OCaml or WhyML language. These properties are assumed to be provided as executable functions returning a Boolean value, and the tool's architecture (Section 4). This allows OCaml and WhyML developers to contribute to its extension.

A major direction of future work is to design and implement mechanisms to automate the generation of properties to be tested, from formal not-yet-proved lemmas or function contracts, when it is reasonably feasible. For function contracts, this generation would work as a verication condition generator in the deductive verication method, with the dierence that the generated verication conditions would have to be executable. AutoCheck has to be extended before pretending to compete with industrial tools such as Quviq [46], the commercial version of QuickCheck. The presented certication of enumeration programs should be extended to the entire code. Data enumeration should be generalized to user-dened datatypes. The specication and certication of more ecient enumeration programs may also be explored. Another direction could be to integrate fuzzing, which has become very popular for property testing [START_REF] Herdt | Verifying instruction set simulators using coverage-guided fuzzing( * )[END_REF][START_REF]An introduction to fuzzing OCaml with AFL, Crowbar and Bun[END_REF] and even coverage-guided fuzzing [START_REF] Padhye | JQF: Coverage-guided property-based testing in Java[END_REF] which makes random testing more ecient.

First

  things rst, what is property-based testing? A property of a program is an observation that we expect to hold true regardless of the program's inputs. It may involve only the output (always outputs a positive number) or compare input and output (preserves list length)

  Each generator is composed of two enumeration functions, declared and formally specied in WhyML in Listing 1.1. A constructor create_cursor initiates the cursor with the rst element of length n of the iteration. A function next replaces the data in the cursor with the next one, if it exists. Otherwise, it sets the eld c.new to false. val create_cursor (n: int) : cursor requires { n ≥ 0 } ensures { result.new → sound result } ensures { result.new → min result.current } val next (c: cursor) : unit requires { sound c } ensures { c.new → sound c } ensures { c.new → lt (old c.current) c.current } ensures { c.new → inc (old c.current) c.current } ensures { not c.new → max (old c.current) } Listing 1.1. Enumeration functions and their contracts.

  function. The function next computing the next permutation in lexicographic order is presented in the Listing 1.3. Its contract species the soundness, progress and completeness properties by one precondition (line 2) and four postconditions (lines 3-6).For n = 2, repetitive calls to the function next, starting from the array 0 1 2 generated by the function create_cursor, generate (in place, in the cursor c) the arrays 02 1 , 1 0 2 , 1 2 0 , 2 0 1 and 2 10 . let next (c: cursor) : unit requires { sound c } ensures { sound c } ensures { c.new → lt (old c.current) c.current } ensures { c.new → inc (old c.current) c.current } ensures { not c.new → max c.current } = let p = c.current in let n = p.length in label L in if n ≤ 1 then c.new ← false else let ref r = (n-2) in while r ≥ 0 && p[r] > p[r+1] do invariant { -1 ≤ r ≤ n-2 } invariant { is_dec_sub p (r+1) n } variant { r+1 } r := r-1 done; if r < 0 then c.new ← false else let ref j = (n-1) in while p[r] > p[j] do invariant { r+1 ≤ j ≤ n-1 } invariant { all_lt p r j } (* p[j+1..n-1] < p[r] *) variant { j } j := j-1 done; swap p r j; reverse p (r+1) n; assert { lt_at (p at L) p r }; c.new ← true Listing 1.3. Second enumeration function for a generator of permutations.

  eld of the cursor (line 22). The loop invariant on Line 17 states that the subarray p[r + 1..n -1] is decreasing. The loop invariant (all_lt p r j) on Line 27 states that all values in the subarray p[j+1..n-1] are strictly lower than p[r]. Consequently, the value p[j] after the loop is the smallest value greater than or equal to p[r] in the subarray p[r + 1..n -1], so the swap and the reverse after the loop minimally increase the array, a key argument to prove the completeness property. In the assertion on Line 33 (p at L) denotes the permutation p at the beginning of the function (Line 10). The assertion states that the subarrays (p at L)[0..r-1] and p[0..r-1] are equal and that (p at L)[r] < p[r].With these annotations, auto-active verication of the soundness, progress, min and max properties succeeds. However an interactive proof in Coq was required to prove the harder property of incrementality. An intermediate version of this work, without the proof of completeness, has been presented during a French conference[START_REF] Giorgetti | Preuve de programmes d'énumération avec Why3[END_REF].

3. 3

 3 Enumeration by ltering Assume you already have implemented, specied and certied an enumeration program for some family of data. Then an enumeration program for those data that satisfy an additional constraint can easily be implemented by running your program and selecting among its outputs those satisfying that constraint. Of course, the more data are rejected, the less eective is the resulting program. However, we have shown in a former work [18, Sect. 3.2] that this ltering technique provides a specication, an implementation and a certication of the resulting enumeration program almost for free.3.4 Contents of ENUM 1.3

Fig. 1 .

 1 Fig. 1. AutoCheck workow.

  5. A user-dened function for Boolean equivalence.

  1 http://why3.lri.fr/stdlib/bool.html.Let us implement a Boolean function for equivalence and test this new function. Function equivb in Listing 1.5 is implemented by using the Boolean function notb for negation. In order to check this implementation, let us now test that this equivalence corresponds to the conjunction of two implications. This relational property about the Boolean functions equivb, andb, implb and notb is implemented by the function equivb_prop on Lines 1-7 in Listing 1.6, taking a pair of Boolean values as input. In order to test this property (on Lines 11-12 in Listing 1.6) we dene a random generator bool_pair_arbitrary of pairs of Booleans (Listing 1.6, line 9) by specialization of a generic generator QCheck.pair for the Cartesian product of two types, provided for WhyML by AutoCheck, by extraction to a similar generator provided for OCaml by QCheck. let equivb_prop (x : (bool,bool)) : bool = let (a,b) = x in match andb (implb a b) (implb b a) with | True → equivb a b | False → notb (equivb a b) end let bool_pair_arbitrary = QCheck.pair QCheck.bool QCheck.bool let equivb_test = QCheck_runner.run_tests (Test.make bool_pair_arbitrary equivb_prop) Listing 1.6. Test of the relational property equivb_prop about the function equivb. The execution output success (ran 1 tests) indicates a successful test. The property has been tested by generating 100 test data and no counterexamples have been found. The complementary output ran 1 tests between parentheses, also produced by the third-party tool QCheck, can be confusing. It does not mean that the property has only been tested once, but that only one property has been tested. The default number of 100 test data can be changed by using the function Test.make_count instead of Test.make. For instance, the code let equivb_test = QCheck_runner.run_tests ( Test.make_count bool_pair_arbitrary equivb_prop 10000) denes a test of the equivb_prop property by random generation of 10000 data. As detailed in Listing 1.8, let us now use the new executable property equivb to check the commutativity property of the orb function for disjunction, whose denition is recalled in Listing 1.7. let function orb (x y : bool) : bool = match x with | False → y | True → True end Listing 1.7. Function orb. let orb_commut_prop (x: (bool,bool)) : bool = let (a,b) = x in equivb (orb a b) (orb b a) let orb_commut_test = QCheck_runner.run_tests ( Test.make bool_pair_arbitrary orb_commut_prop) Listing 1.8. Test of the property orb is commutative.

  lemma Abs_gt0: ∀ x:int. abs x > 0 let wrong_abs_pos_prop (n: int) : bool = abs n > 0 let wrong_abs_pos_test1 = QCheck_runner.run_tests ( Test.make QCheck.(int_range (-100000) 100000) wrong_abs_pos_prop) let wrong_abs_pos_test2 = QCheck_runner.run_tests ( Test.make QCheck.(int_range (-10) 10) wrong_abs_pos_prop) Listing 1.9. Test of a wrong property, mutation of lemma Abs_pos. The rst test (lines 5-6) uses the random integer generator QCheck.int_range with a large interval, and thus passes almost always without nding a counterexample. The second test (lines 8-9) uses the same generator with a smaller interval, and thus almost always fails. For example, when running several times, the test failed 6 times out of 10 for the interval [-100..100], and only once out of 10 for the interval [-1000..1000]. The duration of both tests is about half a second. Now, let us check lemma Abs_le: ∀ x y:int. abs x ≤ y ↔ -y ≤ x ≤ y from Why3's standard library. We turn it into an executable property abs_le_prop (Listing 1.10, lines 1-4) which uses the previously dened Boolean equivalence equivb. A generator of pairs of bounded integers is dened on Lines 6-9. This makes the test on Lines 11-12 more readable. let abs_le_prop (n: (int, int)) : bool = let (x,y) = n in equivb (abs x ≤ y) (-y ≤ x ≤ y) let pair_int_arbitrary = QCheck.(pair QCheck.(int_range (-100) 100) QCheck.(int_range (-100) 100)) let abs_le_test = QCheck_runner.run_tests ( Test.make pair_int_arbitrary abs_le_prop) Listing 1.10. Test of Lemma Abs_le.

  module Option type option 'a = None | Some 'a let predicate is_none (o: option 'a) ensures { result ↔ o = None } = match o with None → true | Some _ → false end end Listing 1.11. Denition of (option 'a) in Why3.

  denition let predicate is_nil (l: list 'a) ensures { result ↔ l = Nil } = match l with Nil → true | Cons _ _ → false end to characterize the empty list Nil.

  let rec function for_all (p: 'a → bool) (l: list 'a) : bool = match l with | Nil → true | Cons x r → p x && for_all p r end Listing 1.14. Executable function for_all from Why3's standard library. As an example, let us consider lists of integers and the parity property that all list items are even. The parity of an integer is dened by the side-eect free function is_even on Line 1 of Listing 1.15. The parity property is implemented on Line 2 and tested on Lines 3-4. let is_even (n: int) : bool = mod n 2 = 0 let for_all_prop (l: list int) : bool = for_all is_even l let for_all_test = QCheck_runner.run_tests ( Test.make QCheck.(list QCheck.int) for_all_prop) Listing 1.15. Parity of all items in a list of integers.

  val function make (n: int) (v: 'a) : array 'a requires { [@expl:array creation size] n ≥ 0 } ensures { ∀ i:int. 0 ≤ i < n → result[i] = v } ensures { result.length = n } Its second postcondition can be tested with random lengths in [0..1000] as follows: let length_make_prop (n: int) : bool = length (Array.make n 0) = n let length_make_test = QCheck_runner.run_tests ( Test.make QCheck.(int_bound 10000) length_make_prop) This is an example of relational property about arrays whose test does not require any array generator. AutoCheck species for WhyML the following two array generators: val function array_of_size (n: Gen.int) (a: arbitrary 'a) : arbitrary {array 'a} val function array (a: arbitrary 'a) : arbitrary {array 'a} They are extracted to the OCaml array generators array_of_size : (RS.t → int) → 'a arbitrary → 'a array arbitrary array : 'a arbitrary → 'a array arbitrary

6. 1

 1 Elementary example for WhyML AutoCheck provides generators (SCheck.int_range a b) and (SCheck.int_bound n) to enumerate integers in an interval [a..b] or [0..n]. They are used in Listing 1.16 to test by enumeration the wrong lemma shown on Line 1 in Listing 1.9. The rst (resp. second) test nds the counterexample 0 in around 3 seconds (resp. less than 1 second). let wrong_abs_pos_test1 = SCheck_runner.run_tests ( Test.make SCheck.(int_range (-10000000) 10000000) wrong_abs_pos_prop) let wrong_abs_pos_test2 = SCheck_runner.run_tests ( Test.make SCheck.(int_bound 10000) wrong_abs_pos_prop) Listing 1.16. Enumerative tests of Lemma Abs_gt0.

  let function b_range (a: array int) : bool ensures { result ↔ range a } = let n = a.length in for j = 0 to n -1 do invariant { range_sub a 0 j n } if not (in_interval a[j] 0 n) then return false done; true Listing 1.18. Implementation of the predicate range. A loop invariant (on Line 6) helps to prove the postcondition. It uses the following generalization of range which controls that each element of the subarray a[l..u-1] is in the interval [0...b -1]: predicate range_sub (a: array int) (l u b: int) = ∀ i: int. l ≤ i < u → in_interval a[i] 0 b

  providing the test oracle. They can be dened by the user or produced by an external tool.We presented several design choices and illustrated them by an open-source prototype, named AutoCheck. The rst originality of our work is to propose formal specication and formal proofs for the data enumeration programs, thus addressing the certiability issue of automated testing tools. A second methodological proposition is to lighten the development of the tool for the WhyML language, by exploiting an existing extraction mechanism from WhyML to OCaml and a third-party random testing tool for OCaml. Another contribution is a tutorial, with elementary examples, that a beginner can follow to practice property-based testing on the supported types. We also explained code certication (Section 3)

  We characterize these permutation arrays with the predicate predicate is_permut (a: array int) = range a ∧ injective a where (range a) species that the values of array a are in [0...a.length -1] and (injective a) species injectivity of the function represented by a, i.e., uniqueness of values in a.Initialization. The smallest permutation in lexicographical order is the one sorted in ascending order, i.e. the identity function. It is characterized on any subarray a[l..u] by the predicate

predicate is_id_sub (a:array int) (l u:int) =

∀ i:int. l ≤ i < u → a[i] = i

which species that each array value is its index. The function create_cursor (Listing 1.2) returns a cursor initialized with the identity table and the new eld equal to true. let create_cursor (n: int) : cursor requires { n ≥ 0 } ensures { result.new && sound result } ensures { min result.current } ensures { result.current.length = n } = let p = make n 0 in

Table 1

 1 presents the generators in ENUM 1.3 and some metrics about them.The rst column assigns a name to each generator. The number of lines of code (resp. WhyML annotations) is recorded in the second (resp. third) column. The fourth (resp. fth) column gives the number of transformations (resp. lemmas) needed to prove their soundness, progress and completeness properties. All of them have been proved automatically with Why3 1.4.0 and the SMT solvers Alt-Ergo 2.4.0, CVC4 1.6, Z3 4.7.1 and Z3 4.8.10, except the completeness property for the generator of permutations, which required an interactive proof of two lemmas with Coq 8.12.2.

	Array family	Code Specication Transformations Lemmas
	rgf sorted perm barray fact endo	26 22 42 22 22 22	22 26 86 23 20 22	1 4 5 3 1 0	0 0 16 0 0 0
	sorted ⊂ barray 24 24 inj ⊂ barray surj ⊂ barray 34 comb ⊂ barray 17	15 16 25 10	0 0 0 0	0 0 0 0

Table 1 .

 1 Generators in ENUM 1.3.The rst block of lines in Table1concerns eective enumeration programs.The rst four are adaptations of C++ programs proposed in[START_REF] Arndt | Matters Computational -Ideas, Algorithms, Source Code[END_REF]. The program rgf (for restricted growth function) enumerates the arrays a of length n such that a[0] = 0 and a[i] ≤ a[i -1] + 1 for 1 ≤ i ≤ n -1.sorted generates all arrays from {0, ..., n-1} to {0, ..., k-1} sorted in increasing order. perm enumerates the permutations on {0, ..., n -1}. barray (for bounded array) (resp. endo) (for endo-array) enumerates the arrays of length n whose values are in {0, ..., k -1} (resp. {0, ..., n -1}). fact enumerates the n! factorial arrays[START_REF] Giorgetti | Combinatoire formelle avec why3 et coq[END_REF] f of length nThe second block concerns enumeration programs obtained by ltering. We denote by Z ⊂ X an enumeration program of data Z implemented by ltering among more general data X. For instance, sorted ⊂ barray enumerates increasing arrays ltered among bounded arrays. By ltering from barray we get generators for the following data families: arrays sorted in increasing order, injections from {0, ..., n -1} to {0, ..., k -1} for n ≤ k (inj ⊂ barray), surjections from {0, ..., n-1} to {0, ..., k -1} for n ≥ k (surj ⊂ barray), and combinations of n elements selected from k, which are encoded by arrays c of length n such that 0 ≤ c[0] < . . . < c[n -1] ≤ k -1 (comb ⊂ barray).

	Each test in OCaml exploits one or more random or enumerative data genera-
	tors, respectively dened in the third-party random testing tool QCheck (whose
	main le is QCheck.ml ) and in our enumerative testing prototype for OCaml
	(whose main le is SCheck.ml). As detailed in Section 6.2 the latter encapsulates
	several enumeration programs from release 1.3 of ENUM library. This OCaml
	code, gathered in the le Enum.ml, is automatically extracted by Why3 from
	WhyML enumeration programs whose properties are proved with Why3, as de-

such that 0 ≤ f [i] ≤ i for 1 ≤ i ≤ n -1.

4 AutoCheck

This section presents the principles, design choices and architecture of our prototype AutoCheck for random and enumerative test data generation and test execution. It is freely distributed at https://github.com/alaingiorgetti/autocheck.

The work presented in this paper corresponds to its pre-release 0.1.2. It contains the most basic functionalities, and is intended to be completed collaboratively in the coming years.

AutoCheck has been designed with simplicity (for users, but also for tool authors) and usability as highest priority. Firstly, a Dockerle is provided, making installation as simple as running a system command (provided). The command builds a virtual machine (a container in docker terminology) in which the tool can be executed safely for the host system. Secondly, many examples of tests in OCaml (resp. WhyML) syntax are provided, in a single le named TestExamples.ml (resp. TestExamples.mlw). They are ordered by increasing complexity and they cover all the functionalities of the prototype. Some of these examples are documented in Sections 5 and 6. Moreover, syntaxes for OCaml and WhyML random and enumerative tests have been chosen to be as similar as possible.

The prototype workow is depicted in Fig.

1

. AutoCheck itself is represented by the largest rectangle with rounded corners. Automatically generated les are represented by dashed rectangles. Each AutoCheck's input is represented by a rectangle with square corners. It is either a WhyML or an OCaml le (respectively named Tests.mlw or Tests.ml in the gure) containing the implementation under test and a description of tests. Since the properties to be tested and their tests respectively are ordinary OCaml or WhyML executable functions and function calls, and since OCaml and WhyML applications can be made up of multiple les, the implementations under test, their properties and the tests of these properties can be in a single le or provided in multiple les.

  To illustrate counterexample generation, let us start with the false property () is not an inhabitant of unit. The property is implemented by the function is_unit_prop reproduced on Lines 1-2 Listing 1.4. Test of a false property about the unit type. The test (on Lines 4-5) is built by the Test.make function, applied to a random generator QCheck.unit of data with type unit, and to the executable property is_unit_prop. The function QCheck_runner.run_tests implements test execution. Assume that the code in Listing 1.4 is in the module RandomTests of the le TestExamples.mlw. Then, the command bash ./why3_check.sh TestExamples RandomTests executes all the tests dened in that module. Here, it generates the following result:

	in the Listing 1.4.
	let is_unit_prop (x: unit) : bool
	= match x with () → False end
	let is_unit_test = QCheck_runner.run_tests (
	Test.make QCheck.unit is_unit_prop)

  The false property that the only inhabitant of type (list 'a) is Nil can be directly tested with is_nil, as shown in

	Listing 1.13. Notice that WhyML lists are polymorphic but a generator of list
	elements (here, QCheck.bool, for Booleans) has to be provided to the test gener-
	ator, xing the actual type of the generated lists.
	let is_nil_test = QCheck_runner.run_tests (
	Test.make QCheck.(list QCheck.bool) is_nil)
	Listing 1.13. Test with is_nil function as property.

  Let us now see how a property on lists can be constructed with the help of the recursive function for_all from Why3's standard library reproduced in Listing 1.14. This function returns true if and only if a given function p returns true for all items in a given list l. So, it provides a Boolean implementation for a family of universal properties over list items.

  Our illustrative example is the function inverse_in_place from the gallery of veried WhyML programs 2 . Its specied header is reproduced in Listing 1.17. The contract specication syntax (requires, ensures) is part of 2 http://toccata.lri.fr/gallery/inverse_in_place.en.html,April 30, 2021 WhyML, its meaning is more detailed in Sect. 3.2. The predicate is_permutation used in this contract is similar to the predicate is_permut presented in Sect. 3.2.The function computes the inverse of its input array, assumed to be a permutation, in place, i.e. in the array itself. It is a specication and implementation in WhyML, by M. Clochard, J.-C. Filliâtre and A. Paskevich, of an adaptation to an array on [0..n -1] of Algorithm I described by D. Knuth for an array on[1..n] in Section 1.3.3, page 176 of The Art of Computer Programming, volume 1[START_REF] Knuth | The Art of Computer Programming[END_REF].It implements the logical predicate is_permutation if the functions b_range and b_injective respectively implement the predicates range and injective dened in Sect. 3.2. We only detail the implementation b_range of the predicate predicate range (a: array int) = ∀ i: int. 0 ≤ i < a.length → in_interval a[j] 0 n A naive (i.e., non-optimized) implementation of the predicate injective is similar. The denition let predicate in_interval (x l u: int) = l ≤ x < u is a specicity of WhyML. It is indeed both a logical predicate and an executable function, because it is also the case for the comparison operators ≤ and < on integers. Thus, it can be used in a specication and in a program.The function b_range in Listing 1.18 implements the predicate range. The universal quantication is implemented by a for loop that stops at the rst array value not in the interval [0..n -1]. The postcondition (on Line 2) ensures that the function implements the logical predicate range: the function returns true if and only if the predicate holds for the input array a.

	let inverse_in_place (a: array int)
	requires { is_permutation a }
	ensures { is_permutation a }
	ensures { ∀ i. 0 ≤ i < length a → (old a)[a[i]] = i }
	Listing 1.17. Inversion of a permutation in place, function contract.
	Here we do not intend to explain the code it is well done in the provided ref-
	erences but to test by enumeration its following two properties, corresponding
	to the two postconditions in Listing 1.17:
	tributed with Why3 1.4.0 3 is made up of seven universal formulas and occupies
	ten lines of code. Second, Why3's most advanced automated proof strategy,
	named Auto level 3, does not overcome this proof. It is completed by an inter-
	active proof step, applying the transformation split_goal_right. Thus, before
	looking for an interactive proof of these properties, it is relevant to test them.
	Enumerative test session. Let us now detail how to test (P 1 ) by enumeration
	with AutoCheck, and how it works internally. The postcondition (is_permutation a)
	is not executable. In order to test it, the logical predicate is_permutation has to
	be implemented by an executable function returning a Boolean value, such as
	the following one:
	let b_permutation (a: array int) : bool = b_range a && b_injective a

(P 1 ) The function inverse_in_place preserves permutations. (P 2 ) The function inverse_in_place computes in place the inverse permutation of its input.

Let us rst observe that the deductive verication of these properties is highly non-trivial. First, the loop invariant proposed in the version of this example dis-

  Then, an enumerative test of (P 1 ) with all permutations of size 6 is let inverse_in_place_permut_test = SCheck_runner.run_tests ( Test.make SCheck.(permut_of_size 6) inverse_in_place_permut_prop) An important limitation of Why3 at work here is that the second parameter of Test.make, as a function, should be without side eect. So, a simpler version of inverse_in_place_permut_prop, such as let inverse_in_place_permut_prop (a: array int) : bool = inverse_in_place a; b_permut a would not be accepted, since it modies the input array a. The functions SCheck_runner.run_tests, Test.make and Scheck.permut_of_size are automatically extracted into OCaml functions with the same names. The OCaml function Test.make builds a test case by assembling a serial and an executable property. A serial is an OCaml record grouping a printer of integer arrays, borrowed from the third-party tool QCheck, and a data generator.

In the folder https://gitlab.inria.fr/why3/why3/-/blob/1.4.0/examples.

Acknowledgements

The authors would like to thank the anonymous referees for their relevant suggestions. This work has been supported by the EIPHI Graduate School (contract ANR-17-EURE-0002).


Arithmétique sur divers systèmes embarqués aux ressources contraintes : les nombres à virgule fixe

J.-M Friedt, Université de Franche-

Introduction

Bien que le développement sur Raspberry Pi, Beagle Bone ou Redpitaya soit actuellement qualifié d'embarqué, la majorité des systèmes faibles coûts mais surtout faible consommation restent architecturés autour de processeurs aux performances bien plus modestes, ne serait-ce que comme gestionnaire d'énergie et de périphériques [START_REF][END_REF]. Nombre de ces processeurs ne sont pas équipés de périphériques de calcul matériel sur des nombres à virgule flottante dont les opérations doivent être émulées par logiciel. Cette représentation des nombres n'est pas naturelle pour une unité de calcul logique et arithmétique (ALU) qui est optimisée pour traiter des nombres entiers. La majorité des problèmes physiques permettent d'ajuster les unités pour manipuler des valeurs du même ordre de grandeur, qu'une simple homothétie permet de considérer comme des entiers. Il s'agit de l'arithmétique des nombres à virgule fixe. Cependant, contrairement à l'arithmétique des nombre entiers qui est exacte, l'arithmétique des nombres à virgule fixe va souffrir d'inexactitudes liées aux pertes des bits de poids faibles lors de certaines opérations. Rappel : nombre à virgule flottante L'Unité Arithmétique et Logique (ALU) d'un processeur sait naturellement exprimer des opérations logiques ou arithmétiques sur des nombres entiers, positifs ou éventuellement négatifs dans une représentation binaire en complément à deux. Dans cette représentation, la valeurs codées sur N bits sont restreintes à [0 : 2 N -1] en non-signé ou [-2 N -1 : 2 N -1 -1] en signé. La représentation en virgule flottante [START_REF]Floating-Point Arithmetic[END_REF] vise à représenter une gamme plus vaste de valeurs, au détriment de l'exactitude des calculs. Ainsi, les N bits d'un entier sont découpés en deux segments que son, dans une notation scientifique de la forme M × 2 E , une mantisse M < 1 et un exposant E. Si, comme c'est la cas en simple précision, un bit est dédié au signe, 8 bits à l'exposant et 23 bits à la mantisse, alors des grandeurs comprises entre 2 -128 à 2 127 peuvent être représentées (en réalité -126 et non -128), les fameux 10 ±38 . Les 11 bits d'exposant en double précision sont plus faciles à interpréter puisque 2 (2 10 ) = 2 1024 2 10×100 = (2 10 ) 100 (1000) 100 = (10 3 ) 100 = 10 300 . Malgré cette grande dynamique de représentation, les opérations sur les nombres à virgule flottante impliquent d'aligner la virgule -comme nous le ferions en posant une addition à la main -avec une perte de précision résultant du nombre fini de bits pour représenter la mantisse. Les exemples d'imprécisions des calculs en virgule flottante sont bien connus mais apparaissent dans des cas aussi simples que int main() {volatile float f1=0.1,f2=10.; volatile double d1=0.1,d2=10.; int k; for (k=0;k<1000;k++) {f2+=f1; d2+=d1;} printf("%f %lf %0.9lf\n",f2,d2,(double)(d2-f2)); } qui répond : 109.998894 110.000000 0.001106262, soit une différence de 10 -3 sur les mêmes calculs effectués en simple ou double précision (qui donne la bonne solution ici). L'erreur sera d'autant plus grande que les ordres de grandeurs manipulés sont importants, un cas classique de la moyenne glissante qui commence par sommer des termes du même ordre de grandeur mais finit avec un accumulateur important auquel on ajoute une petite valeur en fin de calcul. Ces problème deviennent dramatiques pour les systèmes chaotiques que nous avons volontairement proposé d'illustrer ici -le chaos étant défini par un système dans lequel les erreurs initiales croissent exponentiellement lors des itérations de calculs.

Nous allons aborder ces considérations pour traiter sur microcontrôleurs 8 bits et 32 bits le problème bien connu de la convergence de suites complexes qui donnent naissance aux factales de Mandelbrot et de Newton.

Dans le premier cas, la question est de savoir pour quelle condition sur c ∈ C la suite z n+1 = z 2 n + c converge, ou dans le cas de divergence quelle est la vitesse de divergence (i.e. au bout de combien de temps le module de la suite dépasse un seuil prédéfini). Dans le second cas, la question est de savoir vers laquelle des 3 racines possibles la méthode de Newton résolvant z 3 -1 converge en fonction de sa condition initiale (la méthode de Newton et la suite résultante seront explicitées en temps voulu). Le premier problème fait intervenir des sommes et produits de complexes sur des nombres de l'ordre de -1 à 1 avec une résolution de l'ordre de 10 -2 . Le second problème sera à peine plus compliqué car il fera intervenir une division (complexe).

Architecture du programme

Notre objectif sera de comparer un même algorithme sur une multitude de plateformes, donc nous pouvons réfléchir dès le début à architecturer le programme pour séparer la partie algorithmique, indépendante du matériel et le coeur de notre analyse, de l'initialisation et l'accès aux ressources de communication spécifiques à chaque plateforme (stdout sous unix, port série compatible RS232 pour processeurs ARM, USB pour processeur Atmel/Microchip). Nous choisissons donc de n'avoir qu'un unique code source contenant l'algorithme avec des stubs vers l'implémentation des initialisations et fonctions de communication dépendantes de chaque architecture (Fig. 1). Ces stubs présentent les mêmes prototypes mais implémentent la fonction recherchée différemment selon l'architecture visée, par exemple par une fonction vide tel que ce sera le cas sous unix pour l'initialisation des horloges. Séparer l'algorithme des accès bas niveau est une bonne pratique pour garantir la pérennité du coeur de compétence -l'algorithme -sans devenir dépendante d'une plateforme matérielle qui deviendra rapidement obsolète [START_REF] Vetter | Striving for Performance Portability of Software Radio Software in the Era of Heterogeneous SoCs, Free Software Radio Devroom[END_REF]. Nous lierons les stubs appropriés en sélectionnant le fichier contenant les codes sources associés à une architecture donnée lors de l'édition de liens par Makefile.

Nous html#Implicit-Variables), -l'inclusion de Makefile.inc dépendant de la cible définie en ligne de commande. Ainsi à coups de ifdef XXX ... else ... endif de make dépendants de la définition de la constante XXX voir de la génération dynamique du nom du greffon inclus include Makefile.$(XXX) il sera possible de dynamiquement modifier la définition du compilateur et de ses options de compilation en fonction de la cible visée. Nous pouvons nous convaincre de cette approche par le Makefile contenant include Makefile.$(XXX) qui peut appeler Makefile.1 ou Makefile.2 selon la valeur assignée à XXX lors de l'exécution en shell de XXX=1 make. Si nous définissons Makefile.1 par (noter que @ évite d'afficher la commande exécutée) all: @echo "1" } et Makefile.2 avec le même contenu en remplaçant le symbole affiché par la règle all, alors nous obtenons comme prévu $ XXX=1 make 1 $ XXX=2 make 2

Principe du nombre à virgule fixe

Travailler en nombre à virgule fixe tient simplement en l'idée d'effectuer une homothétie adéquate du problème pour le transformer en nombres entiers. Si un calcul se doit de fournir une température avec une résolution en 0,1 K, alors nous exprimons le problème sur 10 fois la température et nous manipulerons des entiers. Cependant, contrairement à l'arithmétique sur les nombres entiers, exacte car conservant les bits de poids faible au risque du dépassement de capacité sur les bits de poids fort, l'arithmétique en virgule fixe maintient constant le nombre de décimales après la virgule. Cela n'impacte pas la somme : la somme de deux nombres plaçant la virgule à une position connue de la représentation fournit un résultat avec la virgule à la même position. Donc si deux nombres a et b en virgule fixe ont effectué (en base 10 pour simplifier) une homothétie de 10 N , la somme s suit simplement s = a + b en gardant ce facteur d'homothétie 10 N (273,1 K+0,7 K=273,8 K et nous gardons toujours une décimale). Le produit est moins intuitif pour le physicien puisque l'unité de la grandeur manipulée n'est pas conservée (le produit de deux températures en K est exprimée en K 2 ) mais d'un point de vue arithmétique, l'opération diffère du calcul sur les entiers en ce que cette fois des bits de poids faible seront éliminés afin de conserver le même nombre de chiffres après la virgule, tronquant ainsi la précision du calcul. Par exemple 1, 1 × 2, 3 = 2, 53 qui s'exprime comme 2, 5 en ne conservant qu'une décimale : si les deux arguments du produit ont subi la même homothétie, le résultat du calcul doit être divisé par ce facteur. Dans notre expression en nombre entiers, 11 × 23 = 253 et il faut diviser (partie entière) par 10 pour ne conserver que la partie respectant notre représentation.

Nous concluons donc par deux fonctions d'addition et de multiplication que sont

La fractale de Mandelbrot

Fort de ces définitions et trois fonctions, efforçons nous de tracer la fractale de Mandelbrot sur microcontrôleur. La fractale [START_REF] Peitgen | Chaos and Fractals : New Frontiers of Science[END_REF][START_REF] Mandelbrot | The Fractal Geometry of Nature[END_REF] de Mandelbrot est une structure géométrique dans le plan complexe issue de l'analyse de la suite z n+1 = z 2 n + c pour chaque point c ∈ C du plan complexe en initialisant z 1 = c. Chaque point c est représenté par deux symboles, selon que la suite converge ou diverge, et en cas de divergence nous indiquerons au bout de combien d'itérations la condition de divergence a été atteinte -en pratique, un module de z n qui dépasse un seuil.

Nous nous inspirons, par soucis de rigueur scientifique des bornes exploitées dans [START_REF] Brooks | The dynamics of 2-generator subgroups of PSL(2,C)[END_REF] (Fig. 3, gauche), même s'il suffit de passer quelques minutes sur xaos [8] (Fig. 2) pour identifier les bornes intéressantes dans le plan complexe, du tracé de la publication [START_REF] Brooks | The dynamics of 2-generator subgroups of PSL(2,C)[END_REF] qui se focalise sur l'intervalle réel [-2; 0, 25] et l'intervalle imaginaire [-0, 96; 0, 96] pour rechercher des orbites périodiques. Ici nous allons nous intéresser à un ensemble un peu plus large avec une condition de divergence en établissant que si au bout de 16 itérations le carré du module de |z n | n'a pas dépassé 10, alors la suite converge probablement et nous afficherons le premier symbole. Dans le cas contraire, si le module dépasse ce seuil avant 16 itérations, nous afficherons le nombre d'itérations qu'il a fallu pour atteindre le seuil. L'objectif est de cartographier les valeurs de c pour lesquelles la suite converge et qui font appel aux trois stubs que sont clock setup() et usart setup() ainsi que mon putchar() dont les prototypes sont définis dans uart.h : ces fonctions seront spécifiques à chaque plateforme sur laquelle sera exécuté le code. Dans tous les cas, nous obtiendrons la Fig. 3 (droite).

Code générique

Cas du PC

Un ordinateur exécutant GNU/Linux n'a pas besoin d'initialiser l'horloge ou l'interface de communication puisque le système d'exploitation s'est chargé d'initialiser stdout : ainsi, les fonctions clock setup() et usart setup() sont vides et mon putchar(char c) se résume à {printf("%c",c);} qui aura nécessité d'inclure #include <stdio.h> pour éviter les avertissements de gcc. Nous pouvons ainsi rapidement tester le bon fonctionnement de l'implémentation de l'arithmétique en virgule fixe sans mettre en doute l'implémentation sur seront pas en accord avec simavr configuré pour simuler un coeur à 16 MHz). Dans le mode AVR109 compatible avec la bibliothèque Arduino, on prendra soin à désactiver l'interruption liée à la communication sur bus USB, même si ici les interruptions ne sont pas utilisées.

Nous pouvons nous interroger sur la pertinence d'utiliser des float dans la définition des bornes des boucles sur une architecture ne contenant pas de FPU. Nous allons constater que gcc est malin et précalcule toutes les constantes, même faisant intervenir les flottants, et n'inclut pas l'émulation du calcul sur nombre à virgule flottante si toutes les constantes (entières) peuvent être précalculées. Même en l'absence d'optimisation du code (option -O0 de avr-gcc) nous constatons (option -g3 pour avoir tous les symboles de déverminage lors de l'affichage du l'assembleur par avr-objdump -dSt executable.elf), que les bornes de

Temps d'exécution

Tous les temps d'exécution s'obtiennent en prenant soin d'éliminer toute communication -excessivement lente -et répéter chaque calcul itérations fois pour obtenir des temps d'exécution en seconde facilement mesurables. Compte tenu de la vaste différence de puissance de calcul des coeurs de processeurs considérés, le nombre de calculs de la fractale de Mandelbrot a été ajusté tel que indiqué en deuxième ligne (Tableau 1).

La fractale de Newton

Le cas de la fractale de Newton est l'opportunité d'appréhender le cas de la division en virgule fixe. La méthode de Newton permet d'efficacement trouver la solution d'une fonction dérivable f (x) = 0 en itérant la suite x n+1 = x n -f (x n )/f (x n ) selon le principe de rechercher à chaque fois l'intersection de la dérivée avec l'axe des abscisses et ainsi converger petit à petit vers la solution. Cette méthode de résolution s'applique au cas f (x) ∈ C. L'étude de la solution vers laquelle converge la suite en fonction du point de départ x 0 ∈ C a donné lieu à la découverte de la fractale de Newton [START_REF] Peitgen | Chaos and Fractals : New Frontiers of Science[END_REF].

Nous allons nous intéresser au cas le plus simple de f (x) = x 3 -1, x ∈ C et tracer la racine vers laquelle la suite converge en fonction de la valeur initiale de x 0 dans le plan complexe compris entre [-1, 4; 1, 44] pour la partie réelle et [-0, 8 : 0, 8] pour la partie imaginaire par pas de 0, 02. Les racines de x 3 -1 sont évidemment exp(j2π/n), n ∈ [0..2] qui se distingueront pour la racine réelle par une partie réelle positive (+1) tandis que les deux racines complexes (-1 ± √ 3)/2 prśentent une partie réelle négative mais une partie imaginaire positive ou négative, fournissant des critères simples de discrimination. La dérivée de z 3 -1 est 3z 2 donc la suite est z → z -(z 3 -1)/(3z 2 ) = (3z 3 -z 3 + 1)/(3z 2 ) = (2z 3 + 1)/(3z 2 ). Le facteur d'homothétie est à peine plus subtil à sélectionner ici que dans le cas de la fractale de Mandelbrot puisque le numérateur est mis au cube, amplifiant les risques de dépassement de capacité de l'entier qui contient z si nous n'y prenons garde avec SCALE trop important.

La fonction qui nous manque dans la bibliothèque de calcul sur les nombres complexes implémentée auparavant est le quotient de deux nombres complexes. L'approche classique pour éliminer la partie imaginaire du dénominateur est de multiplier numérateur et dénominateur par le complexe conjugué * du dénominateur, sachant que z × z * = |z| 2 ∈ R. Le dernier point concerne le facteur d'homothétie : de même que le résultat du produit devait être tronqué des décimales ajoutées par la multiplication, nous devons ici d'abord multiplier le numérateur du facteur d'homothétie pour ne pas perdre de résolution lors du quotient. Le résultat est :

qui confirme que (1 + 8j)/(-2 -j) = -2 -3j et (1 + 6j)/(-1 -j) = -3, 5 -2, 5j.
La convergence sera déterminée par un module suffisamment proche de 1, condition vérifiée par les trois racines.

Figure 5 -Fractale de Newton calculée sur des nombres à virgule flottante pour une partie réelle comprise entre -1,4 et +1,44 par pas de 0,02 et une partie imaginaire de -0,8 à 0,8 par pas de 0,02. Développement de 1/z 2 en série de Taylor Quitte à effectuer des calculs un peu faux, pourquoi ne pas tenter une solution complètement fausse visant à éliminer le calcul de l'inverse 1/z 2 proche de la racine z 1. En effet, nous savons que 1/(1 -x) 2 s'exprime autour de x → 0 comme un développement de Taylor de la forme 1 + 2x + 3x 2 + ... = n n • x n-1 donc en posant z = 1 -x nous avons une solution proche de z → 1. Le calcul de la suite devient donc sous GNU/Octave de la forme

Conclusion

Nous avons proposé une architecture de programme facilement portable d'une architecture à une autre par l'utilisation de stubs implémentant les particularités de l'accès au matériel dans un fichier séparé du programme contenant la partie algorithmique qui reste portable. Nous sélectionnons l'implémentation appropriée lors de l'édition de liens par le Makefile. Ce faisant, nous avons proposé le calcul des fractales de Mandelbrot et de Newton sur architecture 8 bits Atmel/Microchip et sur architectures 32 bits ARM pour une comparaison des performances de calcul entre les implémentations des opérations arithmétiques en virgule fixe et en virgule flottante. Alors que la première solution est fondamentale pour tirer le meilleur parti des microcontrôleurs aux ressources les plus réduites, l'avènement d'unités de calcul flottant même dans des architectures modestes rend le choix délicat compte tenu du compromis entre le temps de développement, les risques de dépassement de capacité, le temps d'exécution et le coût unitaire du composant.

Les codes sources proposés dans cet article sont disponibles à https://github.com/jmfriedt/arithmetique.

Figure 1 -

 1 Figure1-Illustration de l'architecture d'un programme portable sur une multitude d'architectures en séparant clairement la partie algorithmique, portable et indépendante du matériel, de l'implémentation des appels aux ressources de bas niveau (communication, horloges, périphériques de communication) dépendante de chaque architecture. Le lien entre le code portable et l'implémentation spécifique à chaque architecture est faite par les stubs lors de l'édition de lien qui définit dans le Makefile quel fichier d'implémentation lier au code portable pour générer l'exécutable.

Figure 2 -

 2 Figure 2 -Plein de mini-Mandelbrot dans ce zoom sur le nez de l'ensemble de Mandelbrot, avec les coordonnées indiquant que nous manipulerons des valeurs de l'ordre de l'unité avec une résolution de l'ordre de la centaine.

Figure 3 -

 3 Figure 3 -Gauche : graphique publié dans [7] en 1978. Droite : la solution recherchée avec ce programme.

Table 1 -

 1 Temps d'exécution de itérations fractales de Mandelbrot selon le code fourni en section 4.1, en secondes. Droite : photo de famille des plateformes de test. L'Atmega32U4 et le STM32F103 sont montés sur des circuits dédiés, le STM32F407 sur le Discovery Board commercialisé par ST Microelectronics. dans le code de la section 4.1 nous avons préfixé les déclarations de variables du mot clé volatile pour interdire à gcc d'optimiser le code associé à ces variables et éliminer le code mort en l'absence d'affichage. En effet, avr-gcc élime (option -Os) purement et simplement tout le code si nous ne prenions pas ce soin, et une incertitude subsite sur l'interdiction d'optimisation sur volatile montype zr,zi,seuil; puisque le temps d'exécution diffère si ces variables, pourtant au coeur de l'algorithme, ne sont pas déclarées en volatile (colonne simavr, gauche). Le compromis entre optimisation sans éliminer le code utile reste donc subtile. Nous constatons que 1. l'utilisation de la représentation en virgule flottante, émulée en logiciel sur le Cortex M3 sur STM32F1, induit une augmentation dramatique du temps d'exécution en l'absence de FPU, 2. que flottant ou virgule fixe n'a qu'un impact marginal sur le temps d'exécution sur le Cortex M4 du STM32F4 avec un léger gain pour les entiers, 3. que le calcul flottant est plus rapide que le calcul sur 32 bits pour un Atmega32U4 émulé par simavr, une affirmation corroborée sur divers forums puisque ces deux modes de calcul doivent être émulés par logiciel sur le petit coeur 8 bits d'Atmel/Microchip. Les mesures sur simavr, en analysant la trace résultante de la simulation (Fig. 4) et sur microcontrôleur (allumage/extinction d'une LED en début et fin de calcul) ont été effectuées indépendamment, corroborant l'excellent respect du timing de simavr, avec ici les valeurs numériques pour un cadencement à 16 MHz, 4. alors que les coeurs ARM ne bénéficient pas significativement de remplacer la division par 1000 lorsque 3 décimales sont utilisées par rapport à un décalage logique de 10 bits à droite ( 10), le gain en performance dans simavr est significatif.

Figure 4 -

 4 Figure 4 -Trace mémorisée par simavr avec le registre de communication sur le port série et un port généraliste pour estimer le temps d'exécution de l'algorithme lors de la restitution par gtkwave. Les résultats sont en excellent accord avec la mesure sur plateforme matérielle.

Figure 6 -

 6 Figure6-Fractale de Newton calculée sur des nombres entiers sur 32 bits pour une partie réelle comprise entre -1,4 et +1,44 par pas de 0,02 et une partie imaginaire de -0,8 à 0,8 par pas de 0,02.

Figure 8

 8 Figure 8 -Haut : comparaison entre la racine atteinte par le calcul en virgule fixe pour 2 (gauche) et 3 (droite) décimales. Milieu : différence du nombre d'itérations nécessaires pour atteindre la condition de convergence pour la séquence 2z/3 + 1/(3z 2 ) entre le calcul en virgule fixe (gauche avec 2 décimales, droite avec 3 décimales) par rapport au calcul en virgule flottante. Bas : différence du nombre d'itérations nécessaires pour atteindre la condition de convergence pour la séquence (2z 3 + 1)/(3z 2 ) entre le calcul en virgule fixe (gauche avec 2 décimales, droite avec 3 décimales) par rapport au calcul en virgule flottante.

SCALE=1À

  néanmoins élégants et évoluent en fonction du nombre de termes du polynome inclus dans la suite, pour toujours donner une solution autour de 1 mais diverger plus ou moins rapidement en s'éloignant de 1 -ci-dessous la carte de la racine atteinte pour les ordres 2 à 5, avec bleu foncé indiquant l'absence de convergence et bleu-clair la racine 1 + 0j. Pour toutes ces figures, l'axe réel va de -0,2 à 1,4 et l'axe imaginaire de 0 à 1,2 : chaque fois la figure du haut est la solution atteinte avec le développement de Taylor et en bas la solution recherchée avec l'expression complète de la suite.

allons manipuler des complexes formés d'une partie réelle et une partie imaginaire donc il semble évident de définir une structure struct complexe {montype re; montype im;}; et puisque nous allons

  De cette façon, nous passerons dans Makefile en incluant le drapeau -Dfl l'activation ou non des nombres à virgule flottante, et faisons le choix d'utiliser la nomenclature des types étendus des entiers du C fournis dans stdint.h puisque la taille de l'int n'est pas normalisée et dépend de l'architecture sur laquelle s'exécute le code[START_REF]International Standard, Programming languages -C[END_REF] Architecture du MakefileReléguer au Makefile le passage de paramètres de configurations est aisé, mais se pose la question des diverses architectures possibles de Makefile permettant de compiler un même code à destination de diverses cibles, donc en précisant quelle déclinaison de gcc utiliser (pour quelle cible) et quelles options de compilation utiliser :-la solution la plus stupide que nous proposons par simplicité sur le dépôt github qui accompagne cet article : un fichier de configuration Makefile.xxx avec xxx la cible, et exécution par make -f Makefile.xxx. Ce faisant, nous ne profitons pas du dénominateur commun des divers Makefile mais nous contentons de copier-coller un motif de départ pour le décliner vers les diverses cibles, avec la nécessité de corriger tous les Makefile si une erreur est découverte ultérieurement, -un unique Makefile qui reçoit ses arguments du shell en ligne de commande. Ainsi si nous définissons non pas le compilateur par CC=avr-gcc dans le Makefile mais par CC?=avr-gcc, alors l'affectation ne sera effective que si CC n'est pas défini comme variable d'environnement. Ainsi, exécuter CC=arm-none-abi-gcc make écrasera la valeur par défaut de CC avec le nouveau compilateur et

	tantôt
	travailler sur des entiers représentant les nombres à virgule fixe par homothétie, tantôt des nombres à virgule
	flottante, nous proposons une définition conditionnelle
	#include "stdint.h"
	#ifdef fl
	typdef float montype;
	#define SCALE 1.
	#else
	typedef int32_t montype;
	#define SCALE 100
	#endif
	struct complexe {montype re;montype im;};

le binaire généré sera à destination d'un processeur ARM et non AVR. Cependant, cette méthode nécessite d'écraser toutes les variables que sont les drapeaux de compilation CFLAGS et d'édition de liens LDFLAGS, générant des lignes de commande relativement longues et fastidieuses à taper. C'est toutefois l'approche utilisée par Buildroot pour compiler un même code source à destination d'une multitude de cibles. On prendra cependant soin dans ce cas d'éviter la nomenclature de certaines constantes qui ont des valeurs prédéfinies si elles ne sont pas fournies en ligne de commande : c'est le cas de CC (qui vaut cc donc le compilateur à destination de l'hôte, CFLAGS, LDFLAGS ou CXX selon la liste fournie à https://www.gnu.org/software/make/manual/html_node/Implicit-Variables.

  La partie algorithmique du code se résume à itérer la suite z 2 n + c en faisant trivialement appel aux deux fonctions que nous avons créées pour additionner et multiplier deux complexes, et de tester le carré du module pour vérifier si le seuil de divergence est atteint. Ce code se résume aux quelques lignes suivantes

	#include "uart.h"
	#include "stdint.h"
	int main()
	{
	volatile struct complexe tmp,current;
	volatile int n;
	volatile montype zr,zi,seuil;
	seuil=(montype)(10.*SCALE);
	clock_setup();
	usart_setup();
	for (zi=(type)(-1.2*SCALE);zi<(type)(1.2*SCALE);zi+=(type)(0.02*SCALE))
	{for (zr=(type)(-2.0*SCALE);zr<(type)(.85*SCALE);zr+=(type)(.02*SCALE))
	{n=0;
	current.re=zr;
	current.im=zi;
	tmp.re=zr;
	tmp.im=zi;
	do {
	tmp=addcomp(current,mulcomp(tmp,tmp));
	n++;
	}
	while ((modcomp(tmp)<seuil)&&(n<16));
	if (n<16) mon_putchar('0'+n); else mon_putchar(' ');
	}
	mon_putchar('\n');
	}
	}

  avec l'ajout dans denum des termes polynomiaux des plus élevés vers les plus faibles -ici nous avons volontairement commenté les termes d'ordre 4 et 5. Malheureusement cette solution diverge trop rapidement quand z s'éloigne de 1 et ne permet pas à la suite de converger vers une racine. Les figures ci-dessous présentent l'erreur entre le module de la série de Taylor aux 2, 3 et 4ème ordre, en 3D dans le plan complexe et en 2D selon l'axe réel (partie imaginaire nulle avec une solution exacte en 1 + 0j) et pour la cas extrême d'une partie imaginaire de -0, 5j (tracé toujours selon l'axe réel)

	denum=(tmp*2)/3;	% 2/3z
	tmp-=SC;	% 1/(1-x)^around x=0
	%denum=denum+mulcomp(mulcomp(mulcomp(tmp,tmp,SC),tmp,SC),tmp,SC)*5/3; % +4.z^3/3
	%denum=denum+mulcomp(mulcomp(tmp,tmp,SC),tmp,SC)*4/3; % +4.z^3/3
	denum=denum+mulcomp(tmp,tmp,SC); % +3.z^2/3
	denum=denum+2*tmp/3;	% +2z/3
	tmp=denum+SC/3;	% +1/3

int main() {struct complexe num,denum,current,tmp; int n; montype zr,zi;

Remerciements

Les ouvrages de la bibliographie qui ne sont pas librement disponibles sur le web ont été acquis auprès de Library Genesis à gen.lib.rus.ec, une ressource indispensable à nos activités de recherche et développement.

Références

microcontrôleur.

Cas du STM32F1

Le travail sur STM32 s'appuie sur la bibliothèque libre libopencm3 de https://github.com/libopencm3/ libopencm3 et le compilateur arm-none-eabi-gcc disponible en paquet binaire dans Debian/GNU Linux sous le nom de gcc-arm-none-eabi. Une fois ces dépendances installées, les stubs sont implémentés par #include <libopencm3/stm32/rcc.h> #include <libopencm3/stm32/gpio.h> #include <libopencm3/stm32/usart.h> void mon_putchar(unsigned char ch) {usart_send_blocking(USART1, ch);} void clock_setup(void) {rcc_clock_setup_in_hse_8mhz_out_72mhz(); rcc_periph_clock_enable(RCC_GPIOA); rcc_periph_clock_enable(RCC_USART1); } void usart_setup(void) {gpio_set_mode(GPIOA, GPIO_MODE_OUTPUT_50_MHZ, GPIO_CNF_OUTPUT_ALTFN_PUSHPULL, GPIO_USART1_TX); usart_set_baudrate(USART1, 115200); usart_set_databits(USART1, 8); usart_set_stopbits(USART1, USART_STOPBITS_1); usart_set_mode(USART1, USART_MODE_TX_RX); usart_set_parity(USART1, USART_PARITY_NONE); usart_set_flow_control(USART1, USART_FLOWCONTROL_NONE); usart_enable(USART1); } {gpio_mode_setup(GPIOA, GPIO_MODE_AF, GPIO_PUPD_NONE, GPIO9); //TX gpio_mode_setup(GPIOA, GPIO_MODE_AF, GPIO_PUPD_NONE, GPIO10); //RX gpio_set_af(GPIOA, GPIO_AF7, GPIO9); gpio_set_af(GPIOA, GPIO_AF7, GPIO10); usart_set_baudrate(USART1, 115200); usart_set_databits(USART1, 8); usart_set_stopbits(USART1, USART_STOPBITS_1); usart_set_mode(USART1, USART_MODE_TX_RX); usart_set_parity(USART1, USART_PARITY_NONE); usart_set_flow_control(USART1, USART_FLOWCONTROL_NONE); usart_enable(USART1); } 4.5 Cas de l'Atmega32U4/simavr L'assembleur ARM est presque aussi obscur que l'assembleur x86 en mode protégé et l'analyse du code ne permet pas de facilement mettre en évidence les incroyables optimisations amenées par gcc. Au contraire, l'assembleur du petit coeur 8 bits d'Atmel est limpide et compatible avec une analyse des performances au niveau de l'instruction exécutée par l'ALU et donc au cycle d'horloge près. En particulier, l'analyse du code assembleur va nous permettre d'appréhender les opérations prises en charge par le pré-processeur afin de libérer les ressources du processeur au moment de l'exécution. // disable USB in Arduino AVR109 mode } Les premières lignes de code initialisent simavr en l'absence de matériel sur lequel exécuter le code mais ne seront pas inclus dans le firmware transféré au microcontrôleur si ce matériel est disponible. L'exécution dans simavr [START_REF] Friedt | Émulation d'un circuit comportant un processeur Atmel avec simavr[END_REF] s'effectue par simavr -f 16000000 -m atmega32u4 executable.elf avec la génération d'une trace contenant l'évolution du registre de communication sur le port série UDR1 si nous désirons analyser les temps d'exécution. L'initialisation de l'horloge est détournée pour initialiser au plus tôt les fonctionnalités de l'At-mega32U4 fourni en sortie d'usine en mode DFU, à savoir désactiver rapidement le chien de garde et désactiver la division par 8 de la fréquence de cadencement du coeur de processeur (faute de quoi les temps d'exécution ne Nous avons vu que le calcul du cube présente un réel risque de dépassement de capacité : à titre d'exemple, avec trois décimales significatives ma multiplication par 1000 des réels pour exprimer les entiers se traduit par 1000 3 = 10 9 qui nous rapproche dangeureusement des 2, 14 • 10 9 d'un entier 32 bits signé. Nous pouvons nous interroger sur la différence entre une expression de la suite de Newton comme z n+1 =

Cas du STM32F4

pour éviter le calcul du cube. Ce type de prototypage est bien plus simple à mettre en oeuvre sous GNU/Octave, version libre de Matlab, tel que proposé ci-dessous où les deux fonctions de multiplication et division en virgule fixe sont réimplémentées en profitant de ce que GNU/Octave connaisse la notion de complexe (j 2 = -1), tandis que le cas SC = 1 implémente le calcul flottant et SC > 1 la notation en virgule fixe, l'addition étant toujours faite avec les décimales car sans grande importance dans cette suite. Le programme ci-dessous itère sur la résolution (boucle sur SC et sur l'expression de la suite (boucle sur methode) : 49 end % methode

Nous omettons la figure qui compare les deux méthodes dans le cas de l'implémentation en virgule flottante : la racine sur laquelle les deux expressions de la suite et le nombre d'itérations pour converger sont strictement identiques dans les deux cas. Cependant, nous constatons en Figs. 7 et 8 une différence sur la racine identifiée ou le nombre d'itérations nécessaires pour converger selon la résolution de l'expression en virgule fixe et la méthode sélectionnée.