Niklaus (nommé d'après Niklaus Wirth) est le langage utilisé pour illustrer le cours de traitement des langages.
Nous le reprenons comme langage d'application dans ce cours de sémantique.
Note : Le matériel présenté ici est largement adapté de Concrete Semantics de Tobias Nipkow, que je vous invite à visiter pour approfondir le sujet.
Transparents :
- Introduction
- Syntaxe abstraite et domaine sémantique
- Sémantique opérationnelle
- Sémantique dénotationnelle
- Sémantique axiomatique
Fichiers Isabelle : NikausIsabelle.zip
Introduction
Transparents du cours (introduction)
Transparents du cours (sémantique de Niklaus)
Syntaxe concrète de Niklaus
Sémantique des expressions arithmétiques
Exercice
Définir une fonction simplify :: "expression => expression" qui simplifie une expression (somme avec 0, produit par 0 et par 1, opération sur des constantes), et prouver que cette simplification ne modifie pas la valeur d'une expression.
Sémantique des expressions booléennes
Syntaxe abstraite des instructions
On définit un type inductif instruction permettant de représenter la syntaxe abstraite des programmes Niklaus.
Le type state représente l'état de la machine d'exécution.
Sémantique opérationnelle naïve
Sémantique opérationnelle à grand pas
Sémantique dénotationnelle
Sémantique dénotationnelle naïve
Une première tentative de définition d'une fonction qui associe à chaque instruction la relation qu'elle établit entre les états de la machine d'exécution. Cette tentative échoue car la sémantique de la boucle while ne peut pas être définie de cette façon (on ne peut pas prouver sa terminaison).
Sémantique des définitions récursives
On illustre ici le problème du sens que l'on peut donner à une définition récursive à travers l'exemple de la factorielle et de la suite de Syracuse.
Définition d'une fonction récursive comme plus petit point fixe d'un foncteur
La définition usuelle de la factorielle {$\operatorname{fac} = \lambda n. \operatorname{if} n = 0 \operatorname{then} 1 \operatorname{else} n \operatorname{fac} (n-1)$} est récursive. Dans l'exemple ci-dessous, on donne un sens à cette définition en considérant une fonction comme une relation, c'est-à-dire un ensemble de paires d'éléments. À l'aide d'un foncteur {$\operatorname{Fac}$}, on construit une suite de fonctions partielles qui sont des approximations de plus en plus précises de {$\operatorname{fac}$}, et on définit {$\operatorname{fac}$} comme la limite de cette suite, qui est le plus petit point fixe de {$\operatorname{Fac}$}.
L'utilisation de relations entre entiers plutôt que de fonctions nous permet de travailler sur l'ensemble des relations entre entiers qui, muni de la relation d'inclusion, est un treillis complet (toute paire de relation admet une borne inférieure et une borne supérieure (respectivement l'intersection et l'union des relations), ce qui nous permet d'utiliser le théorème de Knaster-Tarski qui garantit que toute fonction croissante sur ce treillis admet un plus petit point fixe.
Sémantique dénotationnelle de Niklaus
Dans cette sémantique, la définition récursive de la boucle while telle que nous l'avions donnée pour la sémantique à grands pas, est traitée de manière similaire à la factorielle : la sémantique du while est définie comme le plus petit point fixe d'un foncteur.
Preuve de l'équivalence entre la sémantique à grand pas et la sémantique dénotationnelle
Nous avons deux définitions de la sémantique de Niklaus, une opérationnelle et une dénotationnelle. On montre ici que ces deux définitions sont équivalentes.
Sémantique axiomatique de Nikaus
Cette sémantique indique comment l'exécution d'une instruction affecte les prédicat valides sur l'état de la machine d'exécution. On exprime cela sous la forme de triplets de Hoare : {$\vDash \{\varphi\} P \{\psi\}$} indique que si la précondition {$\varphi$} est vraie dans un état, et que l'on exécute {$P$} dans cet état, alors la postcondition {$\psi$} est vraie dans l'état de la machine après exécution de {$P$}. Cette définition repose sur la sémantique à grands pas de Niklaus.
Nous allons définir la sémantique axiomatique de Niklaus comme un jeu de règles permettant de dériver des triplets de Hoare. On note {$\vdash \{\varphi\} P \{\psi\}$} le fait qu'un triplet puisse être dérivé selon ces règles :
Exemple de preuve utilisant la sémantique axiomatique
Grâce au jeu de règles de la sémantique axiomatique de Niklaus, on peut prouver la correction d'un programme Niklaus qui calcule le PGCD de deux entiers par soustractions successives :
Les définitions et les théorèmes utilisés dans cette démonstration sont donnés ci-dessous :
Preuve de la consistence et de la complétude des règles
La consistence des règles de dérivation est le fait que tout triplet dérivable est valide, c'est-à-dire que : {$$\vdash \{\varphi\} P \{\psi\} \implies \vDash \{\varphi\} P \{\psi\}$$}
La complétude des règles de dérivation est le fait que tout triplet valide peut-être dérivé des règles : {$$\vDash \{\varphi\} P \{\psi\} \implies \vdash \{\varphi\} P \{\psi\}$$}
La preuve de la complétude fait appel à la notion de plus faible précondition permettant de valider la postcondition après l'exécution d'une instruction :