Leçon 930 : Sémantique des langages de programmation. Exemples. Julie Parreaux
Leçon 930 : Sémantique des langages de programmation. Exemples. Julie Parreaux 2018 - 2019 [1] Nielson et Nielson, Semantics with application. Références pour la leçon Équivalence petit pas et grand pas Complétude de la logique de Hoare Développements de la leçon Plan de la leçon 1 Le langage IMP [1, p.7] 2 1.1 Syntaxe du langage IMP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Sémantique dénotationnelle des expressions . . . . . . . . . . . . . . . . . . . . . 3 2 Sémantiques opérationnelles 3 2.1 Sémantique opérationnelle à grand pas (sémantique naturelle) [1, p.20] . . . . . . 3 2.2 Sémantique opérationnelle à petit pas (sémantique structurelle) [1, p.33] . . . . . 4 2.3 Équivalence des deux sémantiques . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3 Sémantique dénotationnelle [1, p.91] 5 3.1 Sémantique dénotationnelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Théorie du point fixe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.3 Équivalence des sémantiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 4 Sémantique axiomatique (Hoare partiel) [1, p.213] 6 4.1 Triplet de Hoare . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 4.2 Logique de Hoare partielle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 4.3 Correction et complétude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 5 Ouverture 7 Ouverture 7 1 Motivation Défense Qu’est qu’un programme ? Un programme est une suite d’instructions qui à partir d’une entrée vérifiant une précondition donne une sortie vérifiant une postcondition. Ces deux conditions donnent alors la spécification de notre programme. On s’intéresse alors à plusieurs problème. Le premier qui est le plus naturel est de savoir si un programme est correct, c’est-à-dire si celui-ci vérifie sa spécification (quand on lui donne une entrée vérifiant la précondition nous renvoie une sortie qui vérifie la postcondition). Le suivant est de savoir si un programme est équivalent à un autre : si on donne la même entrée aux deux programmes alors on obtient le même résultat. Le troisième problème et le dernier que nous abordons est la preuve de la correction d’une transformation de programmes qui intervient notamment lors de la compilation. On cherche alors à automatiser ces preuves en formalisant et en axiomatisant la sémantique d’un programme (en lui donnant un certain sens). La sémantique d’un langage de programmation c’est un modèle mathématique permettant de raisonner sur le comportement attendu des programmes de ce langages. Une sémantique peut prendre des formes mathématiques variées et nous en présentants quelques unes ici. Ce qu’en dit le jury L’objectif est de formaliser ce qu’est un programme : introduction des sémantiques opé- rationnelle et dénotationnelle, dans le but de pouvoir faire des preuves de programmes, des preuves d’équivalence, des preuves de correction de traduction. Ces notions sont typiquement introduites sur un langage de programmation (impératif) jouet. On peut tout à fait se limiter à un langage qui ne nécessite pas l’introduction des CPOs et des théorèmes de point fixe généraux. En revanche, on s’attend ici à ce que les liens entre sémantique opérationnelle et dénotationnelle soient étudiés (toujours dans le cas d’un langage jouet). Il est aussi important que la leçon présente des exemples d’utilisation des notions in- troduites, comme des preuves d’équivalence de programmes ou des preuves de correction de programmes. 1 Le langage IMP [1, p.7] On travaille sur un langage jouet impératif mettant en place la notion de mémoire via les affectation et la boucle while. 1.1 Syntaxe du langage IMP — Définition : Syntaxe et grammaire du langage IMP — Exemple : Factorielle et Fibonacci (arbre de syntaxe) — Parler de syntaxe concrète vs la syntaxe abstraite Quelques remarques : le parenthésage de notre séquence d’instruction n’est pas fondamen- tal car ils sont tous équivalents car la séquence d’instruction est associative. Contre-exemple quand ce n’est pas le cas ? 2 1.2 Sémantique dénotationnelle des expressions Les sémantiques, ou plus exactement les fonctions sémantiques que l’on définies ici, sont très générique, mais à l’aide des expressions légales on les spécialise comme on le souhaite. — Idée : Les sémantiques dénotationnelles modélisent le comportement par une fonction mathématique. — Définition : Sémantique dénotationnelle des expressions — Sémantique des nombres : N : NUM →Z (on identifie les nombreux aux entiers). — Sémantique des variables (amène la question de la mémoire) : STATE : Var →Z — Sémantique des expressions arithmétiques A et booléennes B (indépendance à la syntaxe + expressivité de nos booléens : on peut exprimer toutes les fonctions boo- léennes) . — Remarque : On suppose State totale (toutes les variables sont définies et on les initialise à 0 ; même si elle pourrait être partielle , fait l’impasse sur les cas d’erreurs) + représenta- tion avec liste finie. — Exemple : s = [x 7→3] ; AJx + 1Ks = 4 et BJ¬(x = 1)Ks = tt. — Remarque : totalité des fonctions A et B + contre-exemple : ajout d’une opération binaire de division. Quelques notions : la notion de variable libre toutes les variables que l’on considères sont libres et de substitution : on souhaite décrire certaines propriétés sur nos sémantiques future : ces notions permettent de formaliser deux concepts : la portée d’une variable (lorsqu’on a des fonctions ou des blocs) et la dépendance syntaxique (est-on atteint par la substitution)). Ces notions ne sont pas nécessaires car on suppose que toutes les variables sont libres et on n’utilise pas la notion de substitution. 2 Sémantiques opérationnelles Idée : Les sémantiques opérationnelles modélisent le comportement par un système de transi- tions dont les règles ⟨S, s⟩→s′ modélisent le fait "l’exécution de S sur l’état s termine dans l’état s′". 2.1 Sémantique opérationnelle à grand pas (sémantique naturelle) [1, p.20] Définition de la sémantique — Définition : règles inductives — Définition : d’arbre de dérivation (Notion de terminaison ?) — Exemple : factorielle Fonction sémantique — Proposition : sémantique déterministe (⇒induction sur la hauteur de l’arbre ; ⇐évident) — Application : IMP est déterministe (Induction sur la structure des instructions) — Contre-exemple : instruction choose et IMP est non-déterministe — Définition : fonction sémantique (fonction car déterministe) (on s’en sert pour mon- trer l’équivalence de programme) Propriétés de notre sémantique — Définition : Équivalence de langage 3 — Exemple while b do S est sémantiquement équivalent à if b then (S; while b do S) else skip (utile dans le DEV 1) et S1; (S2; S3) et (S1; S2); S3 sont sémantiquement équivalents — Contre-exemple : x := 3; x := x ⊕1 n’est pas équivalent à x := x ⊕1; x := 3 Extension du langage repeat until ou for Preuve de programme [1, p.206] Limite : La sémantique à grand pas ne permet pas d’exprimer les interruptions de pro- grammes du à la division par 0 par exemple. 2.2 Sémantique opérationnelle à petit pas (sémantique structurelle) [1, p.33] La sémantique à petit pas ne traite de la terminaison que par la fonction sémantique qui n’est pas toujours facile à manipuler. La sémantique à petit pas vient combler ce manque. Idée : La sémantique à petits pas est plus fine que la précédente : elle se concentre sur les étapes de l’exécution (affectations et tests). Définition de la sémantique — Définition : règles inductives — Définition : séquence de dérivation Notion de terminaison avec des séquences finies ou non ? — Exemple : factorielle — Structure horizontale qui représente l’évolution temporelle de notre calcul et une structure verticale qui représente les sous calcul que nous devons effectuer. Fonction sémantique — Proposition : Langage déterministe sous la sémantique à petits pas — Application : IMP est déterministe (induction sur k, longueur de la séquence) — Définition : fonction sémantique on s’en sert pour montrer l’équivalence de pro- uploads/s3/ 930-semantique.pdf
Documents similaires










-
30
-
0
-
0
Licence et utilisation
Gratuit pour un usage personnel Attribution requise- Détails
- Publié le Sep 24, 2021
- Catégorie Creative Arts / Ar...
- Langue French
- Taille du fichier 0.1627MB