Imperative programming by refinement in the Coq proof assistant ; Programmation impérative par raffinements avec l'assistant de preuve Coq

This thesis investigates certified programming by stepwise refinement in the framework of the Coq proof assistant. This allows the construction of programs that are correct by construction. The programming language that is considered is a simple imperative language with assignment, selection, sequence, and iteration. The semantics of this language is formalized in a relational and predicative setting, and is shown to be equivalent to an axiomatic semantics in the style of a Hoare logic. The stepwise refinement approach to programming requires that refinement steps from the specification to the program be proved correct. For so doing, we use a calculus of weakest pre-specifications which is a generalisation of the calculus of weakest pre-conditions. Finally, to capture the whole refinement history of a program development, we formalize a design language and a logic for reasoning about program designs in order to establish that all refinement steps are indeed correct. The approach developed during this thesis is entirely mecanised using the Coq proof assistant. ; Cette thèse s’intéresse à la programmation certifiée correcte dans le cadre formel fourni par l’assistant de preuve Coq, et conduite par étapes de raffinements, avec l'objectif d’aboutir à un résultat correct par construction. Le langage de programmation considéré est un langage impératif simple, avec affectations, alternatives, séquences, et boucles. La sémantique associée à ce langage est une sémantique relationnelle exprimée dans un cadre prédicatif plus adapté à un plongement dans la théorie des types, plutôt que dans le calcul des relations. Nous étudions la relation entre d’une part la sémantique prédicative et relationnelle que nous avons choisie, et d’autre part une approche plus classique dans le style de la logique de Hoare. En particulier, nous montrons que les deux approches ont en théorie la même puissance. La démarche que nous étudions consiste à certifier, avec l’aide d’un assistant de preuve, les raffinements successifs permettant de ...