Remerciez-le!

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

semantique Leçon Sémantique des langages de programmation Exemples Julie Parreaux - Références pour la leçon Nielson et Nielson Semantics with application Développements de la leçon Équivalence petit pas et grand pas Complétude de la logique de Hoare Plan

Leçon Sémantique des langages de programmation Exemples Julie Parreaux - Références pour la leçon Nielson et Nielson Semantics with application Développements de la leçon Équivalence petit pas et grand pas Complétude de la logique de Hoare Plan de la leçon Le langage IMP p Syntaxe du langage IMP Sémantique dénotationnelle des expressions Sémantiques opérationnelles Sémantique opérationnelle à grand pas sémantique naturelle p Sémantique opérationnelle à petit pas sémantique structurelle p Équivalence des deux sémantiques Sémantique dénotationnelle p Sémantique dénotationnelle Théorie du point ?xe Équivalence des sémantiques Sémantique axiomatique Hoare partiel p Triplet de Hoare Logique de Hoare partielle Correction et complétude Ouverture Ouverture CMotivation 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 introduites comme des preuves d ? équivalence de programmes ou des preuves de correction de programmes Le langage IMP p On travaille sur un langage jouet impératif mettant en place la notion de mémoire via les a ?ectation et la boucle while Syntaxe du langage IMP ?? Dé ?nition Syntaxe et