Vérification formelle d'extractions de racines entières
Nous décrivons la vérification formelle d’algorithmes de calcul de racines carrées, cubiques et énièmes dans un cadre fonctionnel. Nous montrons que les premiers algorithmes se décrivent bien en utilisant la représentation binaire des entiers, qui permet en outre d’assurer la terminaison de ces algorithmes. La même structure est sous-jacente à l’algorithme de racines
énièmes, mais la terminaison de l’algorithme est vérifiée en utilisant des outils plus complexes. Le travail de vérification formelle a été effectué en utilisant le système Coq.
This paper describes the formal verification of algorithms to compute square roots, cubic roots, and nth roots in a functional framework. We show that the first algorithms are easily described by using the binary representation of integers, a solution that moreover makes it possible to ensure the termination of these algorithms. The same algorithm structure underlies the algorithm for nth roots, but ensuring that it terminates requires more complex tools. The formal verification work was done using the Coq system.
Y.BERTOT
vérification formelle de logiciels, calcul des constructions, arithmétique des ordinateurs, Coq.
formal software verification, calculus of constructions, computer arithmetics, Coq.
Français
|
