Le but de ce cours est d’illustrer sur un exemple les fonctionnalités du langage de spécification Gallina associé au Calcul des Constructions Inductives et implanté dans l’assistant à la démonstration Coq.
L’exemple choisi traite de la sémantique d’un mini-langage de programmation impératif (typage, évaluation et sémantique axiomatique). Plusieurs solutions à la modélisation des différentes notions sont proposées. Les différentes constructions utilisées dans ce chapitre seront expliquées plus en détail dans les prochains cours.
Gallina est le nom donné au langage de spécification de l’assistant Coq. Il permet de définir:
Ces caractéristiques du langage le rendent particulièrement adapté à la formalisation des mathématiques et notamment de l’informatique théorique.
On pourra notamment se faire une opinion sur ce slogan en consultant
sur la page de
Coq la liste des développements réalisés par les
utilisateurs.
Les définitions intervenant en sémantique des langages se
représentent particulièrement bien en Gallina:
Nous détaillons ici la formalisation de la sémantique d’un petit langage de programmation dans le style impératif.
Ce genre de formalisation (aussi appelé plongement profond) constitue une alternative à la preuve de programme impératif. Une autre alternative est le plongement simple (aussi appelé plongement superficiel) qui simule les propriétés des programmes impératifs à partir de leur interprétation dans un langage purement fonctionnel. La sémantique est alors implicite dans la traduction. Cette question sera évoquée dans le chapitre traitant de la preuve de programmes impératifs.
Notre langage comprend les commandes suivantes, à partir d’un ensemble de variables X :
Les expressions sont formées de constructions entières et booléennes simples et sont données par la syntaxe de la figure 2.2.
E ::=
Xs Variables sortées | true | false Constantes booléennes | E1 xor E2 Ou exclusif | n Constantes entières | null E Teste si un entier est nul | E1 op E2 Opération binaire sur les entiers s ::= nat | bool op ::= + | − | * | …
Figure 2.2: Syntaxe des expressions
On cherche à définir des sémantiques statiques, opérationnelles naturelles et axiomatiques pour ce langage. Toutes sont représentées en sémantique naturelle par la définition d’une relation entre un programme et des “valeurs”. Cette relation sera décrite à l’aide des règles d’inférence.
Il s’agit de déterminer de manière statique sans l’exécuter qu’un programme est bien formé. Ici il faut vérifier que dans les expressions conditionnelles ou de boucle, les tests sont faits sur des expressions booléennes. Cela nous amène à définir une relation de typage sur les expressions. Les deux valeurs seront les deux sortes nat et bool.
La relation de typage E:s est définie par les axiomes et règles de la figure 2.3.
Xs:s true:bool false:bool n:nat
E1:bool E2:bool E1 xor E2:bool
E:nat null E:bool
E1:nat E2:nat E1 op E2:nat
Figure 2.3: Sémantique statique des expressions
Pour les commandes, on définit la relation C: ok par les règles de la figure 2.4.
skip: ok
E:s X:= E: ok
C1 ok C2 ok C1;C2: ok
E:bool C1: ok C2: ok if E then C1 else C2: ok
E:bool C: ok while E do C:ok
Figure 2.4: Sémantique statique des commandes
La sémantique opérationnelle définit le programme comme une transformation de l’état de la mémoire. Cette mémoire associe à chaque variable et sorte une valeur qui sera une constante entière n ou booléenne b. Les deux opérations utiles sur la mémoire sont la lecture et la mise à jour: si x est une variable et s une sorte alors m(x,s) représente la valeur de la mémoire pour la variable x et la sorte s, si v est une valeur alors m[x← v] représente la mémoire où la variable x a été mise à jour par la valeur v. On a choisi de ne pas indiquer explicitement la sorte de la variable affectée, celle-ci sera déduite de la sorte de la valeur v.
On a besoin de la relation qui associe à chaque mémoire m et expression E une valeur v représentant le résultat de l’évaluation de E dans la mémoire m. On note cette relation m ⊢ E ▷ v. On utilisera des constantes et des fonctions sur le domaine des valeurs réalisant les opérations booléennes et arithmétiques. Elles seront notées en italique en utilisant le même identificateur que dans la syntaxe: ainsi, à la construction syntaxique xor correspond la fonction sémantique xor .
m ⊢ Xs▷ m(X,s) m ⊢ true▷ true m ⊢ false▷ false m ⊢ n▷ n
m ⊢ E1▷ b1 m ⊢ E2▷ b2 m ⊢ E1 xor E2▷ b1 xor b2
m ⊢ E▷ n m ⊢ null E ▷ null n
m ⊢ E1▷ n1 m ⊢ E2▷ n2 m ⊢ E1 op E2▷ n1 op n2
Figure 2.5: Sémantique des expressions
La relation m ⊢ C ▷ m′ exprime que la commande C s’évalue dans une mémoire m qu’elle transforme en une mémoire m′. On la définit par les règles d’inférence de la figure 2.6.
m ⊢ skip ▷ m
m ⊢ E ▷ v m ⊢ X:= E ▷ m[X← v]
m ⊢ C1 ▷ m1 m1 ⊢ C2 ▷ m′ m ⊢ C1 ; C2 ▷ m′
m ⊢ E ▷ true m ⊢ C1▷ m′ m ⊢ if E then C1 else C2 ▷ m′
m ⊢ E ▷ false m ⊢ C2▷ m′ m ⊢ if E then C1 else C2 ▷ m′
m ⊢ E ▷ true m ⊢ C▷ m1 m1 ⊢ while E do C ▷ m′ m ⊢ while E do C ▷ m′
m ⊢ E ▷ false m ⊢ while E do C ▷ m
Figure 2.6: Sémantique des commandes
Il s’agit d’interpréter les commandes comme des transformations de prédicats, ces prédicats spécifiant des propriétés de la mémoire. Si P et Q sont deux tels prédicats et C une commande, alors on définit une relation {P} C {Q} dont l’interprétation est : l’exécution de C à partir d’une mémoire vérifiant P conduit à une mémoire vérifiant Q.
Nous aurons besoin de transformateurs de prédicats particuliers. La conjonction et l’implication de deux prédicats seront notés par P ∧ Q et P ⇒ Q, si x est une variable et E une expression alors P[x← E] représente le prédicat qui à toute mémoire m associe P(m[x← v]) où v est la valeur telle que m ⊢ E ▷ v. Si w est une valeur alors E=w représente le prédicat qui à tout m associe la propriété v=w où v est la valeur telle que m ⊢ E ▷ v.
La définition de cette relation est donnée par les règles d’inférence de la figure 2.7.
{P} skip {P} {P[X← E]} X := E {P}
{P} C1 {P1} {P1} C2 {Q} {P} C1 ; C2 {Q}
{P ∧ (E=true )} C1 {Q} {P ∧ (E=false )} C2 {Q} {P} if E then C1 else C2 {Q}
{P ∧ (E=true )} C {P} {P} while E do C { P ∧ (E=false )}
P ⇒ P1 {P1} C {Q1} Q1⇒ Q {P} C {Q}
Figure 2.7: Sémantique axiomatique des commandes
On remarque que toutes ces définitions font intervenir des notions définies dans le méta-langage telles que la mémoire, les domaines sémantiques, les opérations sur ces domaines,…
Parmi les propriétés intéressantes à montrer on a:
Nous montrons comment représenter la théorie précédente en Gallina.
On choisit de représenter les variables et les opérateurs binaires par des ensembles paramétriques qui pourront être instanciés dans un second temps. Par contre, les fonctions booléennes sont représentées de manière concrète par un constructeur du type de données. Ce choix permet d’illustrer deux traitements possibles des opérations du langage que l’on cherche à modéliser.
Le prédicat exprcorrect traduit la relation décrite dans la figure 2.3. Chaque règle d’inférence définissant la relation est traduite en un constructeur de la définition inductive. Les variables libres des définitions deviennent des variables quantifiées universellement dans les constructeurs.
Il s’agit de représenter le domaine sémantique des variables, à chaque sorte de variable correspond un ensemble au sens mathématique qui sera représenté par un type de données Coq ici le type des booléens ou des entiers. Le domaine sémantique des valeurs semval est représenté par la somme disjointe des deux types.
Les fonctions sémantiques correspondant aux opérateurs concrets peuvent être explicitement programmées. Par contre la sémantique des opérations arithmétiques (qui sont vues de manière paramétrique) doit être fournie comme un paramètre.
Il nous faudra relier la sorte des expressions et le type de leur interprétation sémantique. Pour cela, on définit sort_val une fonction des domaines sémantiques dans les sortes qui à chaque valeur sémantique associe la sorte correspondante.
On utilisera également une relation compat entre les valeurs et les sortes telle que (compat Sbool v) soit équivalent à ∃ b:bool.v=(Bool b) (défini par le prédicat valbool) et (compat Snat v) soit équivalent à ∃ n:nat.v=(Nat n) (défini par le prédicat valnat).
On remarque que le définition inductive de valbool est un codage inductif direct de la proposition fun x:semval => exists b:bool, x=Bool b. On peut aisément montrer la correspondance entre compat et sort_val.
Une alternative est de représenter la notion de compatibilité par un prédicat inductif :
Les deux définitions sont équivalentes, remarquons que dans le second cas la propriété
| (compat1 Snat v) → ∃ n : nat. v=(Nat n) |
nécessite une inversion du prédicat inductif alors que dans le cas de compat c’est une simple conséquence du calcul de l’expression Cases et de la définition de valnat.
La mémoire est représentée comme une fonction qui à toute variable et sorte associe une valeur sémantique, il faudra de plus supposer que cette valeur est compatible avec la sorte.
Pour construire la relation entre une expression et sa valeur, on peut se donner une mémoire comme paramètre dans une “Section”, lorsque la section est fermée, les notions introduites seront automatiquement abstraites par rapport aux paramètres dont elles dépendent.
La définition exprval formalise la sémantique des expressions telle qu’elle est présentée à la figure 2.5.
On peut maintenant énoncer le théorème qui dit que toute expression correctement typée admet une valeur.
La preuve par récurrence nécessite un lemme plus fort qui dit que la valeur calculée est compatible avec la sorte de l’expression.
Le traitement de la relation entre la sorte de l’expression et le domaine de la valeur sémantique est lourd. On peut profiter de l’expressivité du langage de spécification de Coq pour utiliser d’autres formalisations. On construit une famille dépendante sval (dont le type est sort→ Set) qui à la sorte Sbool associe le type bool et à Snat associe le type nat. Le domaine sémantique semval pourrait être représenté par un couple formé d’une sorte s et d’un objet de type (sval s), ceci revient juste à coder une somme disjointe explicitement à l’aide d’un sélecteur s et d’un champ dont le type varie suivant le sélecteur.
On peut tirer partie de cette représentation pour simplifier la formalisation en rendant implicite dans la définition de la mémoire la notion de compatibilité.
On définit alors:
Le lemme de correction de l’évaluation s’énonce alors simplement :
La formalisation et la preuve sont plus simples cependant l’usage de types dépendants rendra la formalisation de la fonction d’écriture sur la mémoire plus complexe en effet on doit avoir avec n:name,s:sort,v:(sval s),mem:memory1
Le simple fait de savoir que s=s′ ne suffit pas à assurer que le terme v de type (sval s) est aussi de type (sval s′). Il faudra utiliser une analyse par cas suivant les valeurs de s et s′. Une telle analyse n’aurait pas été possible si l’ensemble des sortes était resté paramétrique.
De manière générale, en présence de types dépendants, l’usage de l’égalité devient délicat. Il n’est pas possible par exemple d’écrire v=v′ avec v:(sval s) et v′:(sval s′) sauf lorsque s et s′ sont convertibles, la présence d’une hypothèse s=s′ est insuffisante. Il faudra utiliser des notions plus complexes d’égalité.
On pourrait définir le fait qu’une expression e est mal formée comme la propriété :
| ∀ s:sort.¬ (exprcorrect s e) |
En fait il est plus aisé de manipuler des définitions positives et donc de définir une notion constructive d’expression erronée en énumérant les cas d’échec possibles. Si on s’intéresse à l’interprétation constructive des preuves (que nous verrons plus tard) on remarque qu’une preuve que l’expression erronée permet de retrouver exactement la nature de l’erreur à savoir dans quel sous terme un opérateur a été appliqué à une expression d’une sorte non adaptée.
Le théorème exprimant la décidabilité du typage et de l’évaluation est juste une preuve du fait que pour toute expression E, soit il est possible de construire une valeur v de l’expression dont la sorte est la sorte de l’expression soit il est possible de prouver que l’expression E est mal formée. Le fait d’utiliser une interprétation constructive de la disjonction et de l’existentielle assure l’existence d’un algorithme permettant de décider dans quel cas on est et de calculer effectivement la valeur. On établit un résultat de décidabilité sans avoir à représenter une notion de calculabilité.
Si on ne s’intéresse qu’à la partie calcul de cette preuve alors on a une fonction eval_prog qui à toute expression associe une valeur ou rien du tout. Cette fonction peut également se représenter dans Gallina en utilisant le type option de Coq.
La fonction eval_prog se calcule par point fixe structurel sur l’expression.
La section Valexpr, ouverte page ?? est alors fermée ce qui a pour effet d’abstraire les définitions effectuées dans la section par rapport à memstate et à l’hypothèse memstate_correct lorsqu’elle est utilisée.
La représentation de la syntaxe et de la sémantique statique des commandes suit les définitions des figures 2.1 et 2.4.
Nous définissons maintenant la fonction d’écriture dans la
mémoire. Elle utilise la décidabilité de l’égalité sur les variables,
qui vient de la décidabilité de l’égalité sur les noms (prise comme
axiome puisque l’ensemble des noms n’est pas spécifié) et de celle sur
les sortes qui peut explicitement être construite.
Pour montrer la décidabilité de l’égalité sur un ensemble A,
on peut construire une fonction booléenne f de type A → A →
bool et démontrer que c’est la fonction caractéristique de
l’égalité (f x y)=true ⇔ x=y.
On choisit une autre solution qui est de construire
un terme fdec de type
∀ x,y:A, {x=y}+{¬(x=y)} qui à tous x et y associe soit un
objet (left h) avec h une preuve de x=y soit un objet
(right h) avec h une preuve de ¬(x=y).
Une expression “if a=b then p else q”
s’écrira dans Coq:
match (fdec a b) with left _ => p | right _ => q end.
Ou de manière équivalente :
ifdec (fdec a b) p q
On oublie l’information de preuve pour construire l’expression mais celle-ci pourra être facilement utilisée lorsqu’il s’agira de montrer des propriétés de cette expression.
Nous commençons par poser en axiome la décidabilité de l’égalité sur l’ensemble des noms et nous prouvons la décidabilité de l’égalité sur l’ensemble des sortes.
Nous pouvons définir maintenant l’opération update de mise à jour de la mémoire qui se fait dans une section introduisant le nom de la variable x, la valeur à affecter à cette variable v et la mémoire m. La sorte de la valeur est localement nommée s.
On montre ensuite les propriétés de base de cette fonction :
Après avoir prouvé les lemmes, la section peut être refermée, les constructions sont alors paramétrées par x,v et m.
La déclaration suivante implémente la relation décrivant la sémantique opérationnelle du langage de commande telle qu’elle est décrite dans la figure 2.6.
Nous nous intéressons finalement à la sémantique axiomatique. Une assertion est une propriété de la mémoire, représentée par un prédicat unaire. En logique de Hoare, ce prédicat unaire sera défini concrètement par une formule logique utilisant les variables du programme pour représenter les valeurs correspondantes de la mémoire.
On étend les opérations usuelles de la logique à des transformations d’assertion:
Le transformateur suivant correspond à ce que nous avons noté P[X← E]. Le terme (memupdate x E P) représente le prédicat qui est vrai en m si P(m[X← v]) est vérifié avec v la valeur de l’expression E dans la mémoire m.
On définit le prédicat (trueform P c Q) correspondant à {P} C {Q} telle qu’il est décrit dans la figure 2.7.
Le théorème suivant énonce la correction de la relation donnée {P} c {Q} par rapport à la sémantique.
Les logiques d’ordre supérieur comme le Calcul des Constructions Inductives se prêtent bien aux formalisations de notions sémantiques et logiques. Une des premières preuves de cette nature a été effectuée par Samuel Boutin. Il s’agissait du schéma de compilation d’un mini-ml vers la CAM (Categorical Abstract Machine) tel qu’il était décrit dans l’article [CDDK86]. Yves Bertot a étudié la preuve du compilateur d’un langage impératif vers un langage assembleur [Ber98].
Des preuves de compilateurs plus conséquents ont ensuite été entreprises: Delphine Terrasse [Ter92] a ébauché la preuve d’un compilateur Esterel, Pablo Argon [Arg98] a extrait le noyau du compilateur du langage Electre exprimé comme l’exécution des règles de la sémantique, des équipes de recherche de Dassault et Aérospatiale ont étudié la formalisation d’un compilateur pour le langage Lustre tel qu’il est implanté dans l’outil Scade, une partie de ces développements est disponible domme contribution au système Coq. On trouvera également dans les contributions des formalisations de plusieurs calculs de processus, en particulier le π-calcul ainsi que des modélisations de logique temporelle.
La formalisation de la logique de Hoare a été effectuée par Thomas Kleymann-Schreiber [Sch97, Kle98] dans l’assistant LEGO dont le langage s’apparente au Calcul des Constructions Inductives. Une formalisation dans l’outil HOL a également été réalisée par Peter Homeier, l’objectif principal de ces développements est de justifier les propriétés fondamentales de la sémantique axiomatique comme la correction et la complétude, ce qui n’est pas évident dès que le langage comporte des constructions avancées comme des appels de procédure.
Un domaine actif de recherche est actuellement l’étude des propriétés de sécurité des programmes Java, qu’ils soient utilisés sur l’internet ou les cartes à puce. Pour garantir de telles propriétés, il est essentiel d’avoir une description précise de la sémantique de ce langage, au niveau du code source ou du byte-code, que ce soit la sémantique statique, dynamique ou axiomatique. Le projet Bali #1http://isabelle.in.tum.de/Bali à l’université de Munich formalise ces notions dans l’outil Isabelle/HOL. Des développements analogues sont réalisés à l’aide de Coq en France, dans le projet Lemme à l’INRIA Sophia-Antipolis, dans le projet Lande à l’IRISA ou par la société Trusted Logic. Les définitions inductives sont utilisées de manière intensive dans ces développements.
Lorsqu’on veut étudier les programmes d’un langage X, on peut procéder de deux manières. La première, appelée plongement profond (deep embedding en anglais), consiste à introduire un type concret dans Coq pour représenter les arbres de syntaxe abstraite du langage X. La seconde appelée plongement superficiel (shallow embedding en anglais), consiste à représenter directement un programme de X par sa sémantique exprimée dans le langage mathématique du système Coq.
Dans le plongement profond, on dispose d’un type concret Y qui représente les arbres de syntaxe abstraite du langage X. On peut ensuite construire des fonctions et des relations sur ce type. On pourra ainsi parler des expressions bien formées, construire des algorithmes de typage, représenter la sémantique du langage. Un programme écrit dans le langage X pourra être représenté par un objet Coq de type Y, les propriétés de cet objet seront établies en utilisant différentes sémantiques.
Dans notre exemple, les programmes sont représentés par un plongement profond.
Dans le plongement superficiel, un programme est directement traduit en sa sémantique. Par exemple, on pourrait commencer par introduire une notion de mémoire et identifier un programme à une fonction de transformation des mémoires. La séquence de deux programmes pourrait être définie comme la composition des mémoires les représentant. Les relations sur les programmes comme les sémantiques opérationnelle ou axiomatique peuvent être définies en faisant référence à la sémantique des programmes. Les règles d’inférence deviennent alors des théorèmes qui peuvent être utilisés pour prouver des propriétés de programmes. La représentation des propriétés dans la sémantique axiomatique utilise un plongement superficiel (on n’introduit pas la syntaxe des formules).
Cette représentation peut permettre de raisonner rapidement sur les propriétés de programmes particuliers. Par contre, elle ne permet pas de construire des programmes ou de faire des preuves par récurrence sur la structure des programmes. Elle n’est donc pas adaptée à l’étude méta-théorique des propriétés du langage.