Preuve de correction de programmes fonctionnels de tris dans le systèmes Coq

P. MANOURY

IBP-Litp 1996/22: Rapport de Recherche Litp / Litp research reports
37 pages - Juin/June 1996 - French document.

PostScript : Ko /Kb

Titre / Title: Preuve de correction de programmes fonctionnels de tris dans le systèmes Coq

Résumé : Ce rapport présente une étude de cas de preuve de correction de programmes fonctionnels. Tous les programmes, spécification et preuves ont était développés à l'aide du système d'aide à la démonstration Coq. Les programmes étudiés sont des implémentations de divers algorithmes de tri.
Ce document contient les définitions des structures de données utilisées dans les algorithmes de tri (listes et arbres binaires) et de leurs propriétés attendues. Quelques fonctions auxiliaires sont données ainsi que les propriétés concernant leur usage dans des programmes de tri. Nous définissons ensuite nos divers programmes de tri et décrivons les grandes lignes de leurs preuves de correction. Nous avons étudié cind programmes : le tri par insertion, le tri par funsion, le tri par arbre binaire de recherche, le tri par tas et le tri-bulle. En supplément nous donnons la preuve de correction d'une fonction calculant des arbre binaires équilibrés utilisée dans les tris par fusion et par tas.
L'intérêt de ce rapport vaut moins par l'originalité de ses résultats (les algorithmes présentés sont bien connus) que par son effectivité. Enfin, ce document peut être utilisé comme une bonne introduction pédagogique à la problématique de la correction des programmes.

Abstract : This report is a case study in proving correctness of functional programs. All programs specifications and proofs has been developed with the Coq proof assistant. The programs
investigated are implmentions of variuos sorting algorithm.
The document contains the definitions of data structures involved in sorting programs (lists and binary trees) and their intended properties. Some auxiliary functions are defined and their properties concerning their use in sorting programs are stated. Then we define our various sorting programs and give the broad outlines of the proof of their correctness. We studied five sorting programs : insertion sort, merge sort, binary search tree and heap sorts, bubble sort. As an extra we give the corectness proof of a function building well balanced trees which is used in merge and heap sorts.
The interest of this report is not in its originality (sorting algorithm we present are well known) but merely in its actuality. Also it appears that this document is a good pedagogical introduction to the problematic of programs correctness.

Publications internes Litp 1996 / Litp research reports 1996