Preuve de correction de la traduction des automates en langage B

Preuve de correction de la traduction des automates en langage B

 Présentation de Coq

Coqest un assistant de preuve basé sur le calcul des constructions, un λ-calcul typé d’ordre supérieur basé sur la correspondance de Curry-Howard. Les termes du langage sont des fonctions typées et il est possible d’écrire dans le même langage un programme 73 Chapitre 3. Correction de la traduction et des preuves de propriété sur ce programme. Le langage de programmation de Coq est un langage fonctionnel proche du langage OCaml. Coq permet d’ailleurs d’extraire ses programmes vers OCaml (et vers d’autres langages fonctionnels).

Dans la pratique, le langage Coq permet de définir des types inductifs, comme les types inductifs de OCaml par exemple. Ces types inductifs sont introduits par le mot clé Inductive. Dans la pratique, nous distinguons les types inductifs, qui dans notre traduction permettent de définir les structures du langage (par exemple le type des automates) et les prédicats définis inductivement, appelés dans la suite prédicats inductifs.

Les prédicats inductifs permettent de décrire des prédicats à partir d’un ensemble de règles. Chaque règle est écrite comme une implication : un ensemble de prémisses permettent de déduire un prédicat sur des termes du langage, à la manière des règles d’inférence. Ce sont donc les prédicats inductifs qui permettront de traduire les règles d’inférence des astd. Il faut noter qu’en Coq il n’y a pas de réelle différence de nature entre ces les types inductifs et les prédicats inductifs. La différence réside dans le fait que les prédicats inductifs sont ignorés lors de l’extraction des preuves vers un langage de programmation.

Le langage Coq permet également de définir des fonctions récursives. Ces fonc tions sont introduites par le mot clé Fixpoint. Elles ont deux caractéristiques im portantes : (1) toute fonction doit terminer : l’appel récursif doit porter sur un sous terme structurel de l’argument initial (récursion structurelle) (2) toute fonction doit être totale : la définition d’une fonction récursive se fait généralement au moyen d’une recherche de motif (pattern matching) qui doit être exhaustif.

Enfin, le langage Coq dispose de plusieurs mots clés pour définir des théorèmes (Theorem, Lemma ou encore Corollary) qui doivent ensuite être prouvés. L’écri ture de ces théorèmes est souvent technique et peu compréhensible. Dans ce chapitre, nous avons privilégié une écriture moins formelle qui permet de mieux comprendre les théorèmes prouvés. 

Formalisation

L’objectif de cette section est de présenter la formalisation du problème ainsi qu’une description de la manière dont le problème a été traduit dans le langage Coq,  en décrivant les choix réalisés dans l’implémentation qui impactent les preuves et en explicitant certaines définitions implicites. Dans la section 3.3.1, nous présentons la sémantique formelle des automates dans le langage astd. Puisque les astd ont une sémantique opérationnelle, nous souhaitons avoir une sémantique opérationnelle du langage B. Cette sémantique est décrite dans la section 3.3.2. Les règles de traduction et une description de leur implémentation en Coq sont décrites dans la section 3.3.3. Enfin, le théorème que nous souhaitons prouver est décrit dans la section 3.3.4. 

Sémantique opérationnelle des automates

Le principe des automates dans le langage astd est basé sur le principe des diagrammes d’états hiérarchiques de Harel [Har87]. Un automate est constitué d’un ensemble d’états et d’un ensemble de transitions entre ces états. Le fait que les dia grammes d’états soient hiérarchiques signifie que chaque état de l’automate peut être lui-même un automate. Dans les automates, les transitions peuvent être de trois types : (1) les transitions locales entre deux états d’un automate, (2) les transitions qui partent du sous-état d’un automate et (3) les transitions qui arrivent à un sous-état d’un automate.

Dans ce dernier cas, la transition peut arriver à un état dit historique, c’est-à-dire que l’état après la transition est le dernier état visité. Les automates ont un état initial, marqué par un chevron (>), et un état final marqué par un double cercle. Le type ASTD est le type des astd. L’état courant d’un astd est décrit par le type State. Enfin, l’ensemble des événements acceptés par le système est décrit par l’ensemble Event. La sémantique est décrite par un système de transitions étiquetées, soit un sous-ensemble de State×Event×State.

Une transition du système est un élément de cet ensemble. Elle est notée s σ − →s′,ce qui signifie que dans l’état s, on peut exécuter l’événement σ et qu’après avoir exécuté cet événement, le système est dans l’état s′. Enfin, une fonction appelée final ∈ State → Boolean permet de dire si l’état d’un astd est final et une fonction init ∈ ASTD → State retourne l’unique état initial d’un astd. Dans ce chapitre, nous nous intéressons uniquement à la traduction des automates, les autres opérateurs des astd ne sont pas considérés.