Certification de programmes BSML

Certification de programmes BSML

LA programmation fonctionnelle est un bon cadre de travail pour l’écriture et la preuve de programmes car, sans effet de bord, il est plus simple de prouver la correction des programmes et de les réutiliser en tenant compte de leurs propriétés formelles : la sémantique est dite compositionnelle. Le langage BSML (sans les traits impératifs ni les entrées/sorties) permet de concevoir des programmes parallèles purement fonctionnels. Sa sémantique est aussi compositionnelle. Se pose alors la question de la réalisation de programmes BSML certifiés, c’est-à-dire dont le résultat est toujours celui qui a été spécifié. Ce chapitre traite ce problème et nous utiliserons l’assistant de preuves Coq afin de founir une bibliothèque de fonctions BSML certifiées qui sera un large sous-ensemble de la bibliothèque standard de la BSMLlib. inductives. La théorie des types est un bon cadre pour le développement de preuves de programmes (notam- ment ceux fonctionnels [218]) car elle fournit une grande expressivité logique. Dans l’assistant de preuves Coq, il existe une interprétation constructive des preuves, c’est-à-dire la possibilité de construire automa- tiquement une λ-terme à partir de la preuve d’une formule logique. Ainsi, dans un tel formalisme et grâce à l’isomorphisme de Curry-Howard, une preuve de la formule ∀x.P (x) ⇒ ∃y.(Q y x), appelée une spé- cification, permet d’obtenir un programme correct qui vérifie en entrée la propriété P (une pré-condition) et fournit un résultat qui vérifie Q (une post-condition). Le programme extrait de la preuve (en oubliant les parties logiques de la preuve [220]) est donc garanti par Coq pour bien réaliser la spécification donnée. On parle alors d’un programme certifié.

Nous allons maintenant nous intéresser à la spécification de programmes BSML et à leur développement (réalisation) en Coq. Tout d’abord, nous présenterons rapidement le système Coq (section 6.2). Nous pour- rons alors expliquer comment intégrer les primitives parallèles dans ce système (section 6.3) pour certifier des éléments de la bibliothèque BSMLlib et ainsi obtenir une bibliothèque certifiée (section 6.5).Le mécanisme de construction des preuves n’a pas besoin d’être certifié puisque le noyau du système Coq, c’est-à-dire la fonction de typage vérifie les preuves. Le noyau fait en revanche l’objet de certifications et de vérifications [22]. Ajoutons que la représentation concrète des preuves a d’autres avantages : par exemple, elle rend possible l’écriture d’un vérificateur de type indépendant de Coq, et elle autorise également l’em- ploie de toutes sortes d’outils pour engendrer des preuves que Coq pourra vérifier a posteriori [107].. Il est cependant laborieux de devoir annoter toutes les définitions par des informations de type quand celles-ci semblent pouvoir être aisément déduites du contexte. Coq propose donc un mécanisme simple d’inférence, qui, bien sûr, peut échouer. Coq fournit également un mécanisme d’arguments implicites et il s’efforce aussi de les inférer.Nous nous intéressons donc, dans cette section, au système d’aide à la preuve Coq. Cette section a pour objectif de faire découvrir au lecteur ce système à l’aide d’une rapide description. Bien sûr, cette section n’a pas pour vocation de remplacer la documentation accompagnant le système. Le lecteur pourra donc consulter en complément : le tutoriel et le livre [30] pour une introduction plus graduelle ainsi que le manuel de référence

L’objectif premier de Coq est d’être un assistant de preuves, et donc de permettre de formaliser le rai- sonnement mathématique. Prenons un énoncé basique : ∀A, A ⇒ A. Cet énoncé, qui se lit «pour toute proposition A (c’est-à-dire objet A de type Prop), A implique A», peut être directement transcrit dans le système Coq comme suit :Cette portion de script commence par le nom et l’énoncé de notre lemme, où Prop est l’ensemble des propositions logiques. Le système entre alors dans sa nature interactive qui permet de bâtir cette preuve étape par étape (mot clés Proof). Pour cela, le système utilise des directives appelées tactiques. Celles-ci reflètent la structure de la preuve en déduction naturelle. Nous avons donc : (Calcul des Constructions Inductives) qui est un λ-calcul typé où les énoncés exprimables en Coq sont des types du CCI. En application de l’isomorphisme de Curry-Howard [119], vérifier si t est bien une preuve valide de l’énoncé T consiste à vérifier que le type T est bien un type légal du λ-terme t . C’est ce qui est effectué par le système avec la tactique Qed. Par exemple, si on demande à Coq quelle est la représentation interne du lemme easy à l’aide d’un P r i n t.