From types to logical assertions : automatic or assisted proofs of property about functional programs
Des types aux assertions logiques : preuve automatique ou assistée de propriétés sur les programmes fonctionnels.
Résumé
This work studies two approaches to improve the safety of computer programs using static analysis.
The first one is typing which guarantees that the evaluation of program cannot fail. The functional
language ML has a very rich type system and also an algorithm that infers automatically the types.
We focus on its adaptation to generalized algebraic data types (GADTs). In this setting, efficient
computation of a most general type is impossible. We propose a stratification of the language that
retain the usual characteristics of the ML fragment and make explicit the use of GADTs. The re-
sulting language, MLGX, entails a burden on the programmer who must annotate its programs too
much. A second stratum, MLGI, offers a mechanism to infer locally, in a predictable and efficient way,
incomplete yet, most of the type annotations. The first part concludes on an illustration of the expres-
siveness of GADTs to encode the invariants of pushdown automata used in LR parsing. The second
approach augments the language with logic assertions that enables arbitrarily complex specifications
to be expressed. We check the compliance of the program semantics with respect to these specifica-
tions thanks to a method called Hoare logic and thanks to semi-automatic computer-based proofs.
The design choices permit to handle first-class functions. They are directed by an implementation
which is illustrated by the certification of a module of trees that denote finite sets.
Cette thèse étudie deux approches fondées sur l’analyse statique pour augmenter la sûreté de
fonctionnement et la correction des programmes informatiques.
La première approche est le typage qui permet de prouver automatiquement qu’un programme
s’évalue sans échouer. Le langage fonctionnel ML possède un système de type très riche et un algorithme
effectuant une synthèse automatique de ces types. On s’intéresse à l’adaptation de cet algorithme aux
types algébriques généralisés (GADT), une forme restreinte des inductifs de Coq, qui ont été introduits
par Hongwei Xi en 2003.
Dans ce cadre, le calcul efficace d’un type plus général est impossible. On propose une stratification
qui maintient les caractéristiques habituelles sur le fragment ML et qui isole le traitement des GADT
en explicitant leur utilisation. Le langage obtenu, MLGX, nécessite des annotations de type qui alour-
dissent les programmes. Une seconde strate, MLGI, offre au programmeur un mécanisme de synthèse
locale, prédictible et efficace bien qu’incomplet, de la plupart de ces annotations. La première partie
s’achève avec une démonstration de l’expressivité des GADT pour coder les invariants des automates
à pile utilisés par l’analyse syntaxique LR.
La seconde approche augmente le langage de programmation par des assertions logiques permettant
d’exprimer des spécifications de complexité arbitraire dans la logique d’ordre supérieur polymorphi-
quement typée. On vérifie statiquement la conformité de la sémantique du programme vis-à-vis de ces
spécifications à l’aide d’une technique appelée logique de Hoare qui consiste à engendrer un ensemble
d’obligations de preuves à partir d’un programme annoté. Une fois ces obligations de preuve traitées,
si un programme est utilisé correctement et si il renvoie une valeur alors il est certain que celle-ci est
correcte.
Habituellement, cette technique est employée sur les langages impératifs. Avec un langage fonc-
tionnel pur, les problèmes liés à l’état de la mémoire d’évanouissent tandis que l’ordre supérieur et
le polymorphisme en posent de nouveaux. Nos choix de conceptions cherchent à maximiser les op-
portunités d’utilisation de prouveurs automatiques en traduisant minutieusement les objets d’ordre
supérieur en objets du premier ordre. Une implantation prototype du système en fournit une illustra-
tion dans la preuve presque totalement automatique d’un module CAML d’arbres équilibrés dénotant
des ensembles finis.
Loading...