Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

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 ﬁxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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ériﬁant une précondition donne une sortie vériﬁant une postcondition. Ces deux conditions donnent alors la spéciﬁcation 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ériﬁe sa spéciﬁcation (quand on lui donne une entrée vériﬁant la précondition nous renvoie une sortie qui vériﬁe 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 ﬁxe 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éﬁnition : 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éﬁnies 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éﬁnition : Sémantique dénotationnelle des expressions — Sémantique des nombres : N : NUM →Z (on identiﬁe 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éﬁnies 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 ﬁnie. — 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éﬁnition de la sémantique — Déﬁnition : règles inductives — Déﬁnition : 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éﬁnition : 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éﬁnition : É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 ﬁne que la précédente : elle se concentre sur les étapes de l’exécution (affectations et tests). Déﬁnition de la sémantique — Déﬁnition : règles inductives — Déﬁnition : séquence de dérivation Notion de terminaison avec des séquences ﬁnies 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éﬁnition : fonction sémantique on s’en sert pour montrer l’équivalence de pro- uploads/s3/ 930-semantique.pdf