===== Sémantique Dénotationnelle d'un langage de programmation =====
Consiérons maintenant un langage de programmation impérative simplifié (que nous appellerons "L") comportant :
* instructions de base
* l'affectation : ''x := expr''
* l'instruction vide : ''skip'' ((NOP, mais dans la litterature c'est généralement ''skip''))
* instructions (structures) de contrôle :
* la séquence : ''A;B''
* la conditionnelle : ''if b then A''
* l'alternative : ''if b then A else B ''
* la répétition : ''do n times A''
* l'itération : ''while b do A''
^ Remarque ^
| On s'dresse ici seulement à la sémantique des instruction : sémantique dite __dynamique__ --par opposition à la sémantique __statique__ -- et pas aux déclarations de variable qui p...FIXME...((manque un bout de mot)) ttrait un contrôle de type des expressions sémantique dites statique. |
Nous avons déjà vu que la sémantique d'un programme impératif est une fonction mathématique qui représente l'effet du programme sur un état mémoire :
| f: | ensemble des états mémoire | -> | ensemble des états mémoire |
Cette fonction pren en argument un état mémoire avant exécution et retourne en résultat l'état mémoire après exécution (état initial, état final). Le domaine sémantique du langage "L" est dont l'ensemble des fonctions de S dans S où S est l'ensemble des états mémoire. Donc pour toute instruction "A" de langage "L" :
* \left[\!| A |\!\right] : S \rightarrow S
* s \mapsto s\prime = \left[\!| A |\!\right]\left( s \right)
où s et s' sont des états mémoire, et où un état mémoire est une application de l'ensmeble des identificateurs dans un ensemble de valeurs.
Dans la suite, on notera :
* \left[\!| x |\!\right]_s ou s\left( x \right) la valeur de la variable ''x'' dans l'état mémoire s. Plus généralement, \left[\!| expr |\!\right]_s le résultat de l'évaluation de l'expression ''expr'' dans l'état mémoire s
* \left( s | x \rightarrow v \right) l'état mémoire s mais dans lequel on associe à la variable x la valeur v.
On peut alors établir ces définitions sémantiques :
| l'affectation | \forall s\in S,\quad \left[\!| x := expr |\!\right]\left( s \right) = \left(s | x \rightarrow \left[\!| expr|\!\right]_{s}\right) |
| l'instruction vide | \forall s \in S,\quad \left[\!| skip |\!\right]\left(s\right) = s |
==== Exercice ====
Déterminer la sémantique des programmes :
* P1 : a:= 0; b:= 1
* P2 : b:= 1; a:= 0
\begin{eqnarray}
\forall s \in S & \left[\!| P_1 |\!\right]_s & = & \left[\!| a:=0;b:=1 |\!\right]\left( s\right) \\
& & = & \left[\!| b:=1 |\!\right]\left( \left[\!| a:=0 |\!\right]\left( s \right)\right) \\
& & = & \left[\!| b:=1 |\!\right]\left( s| a \rightarrow 0\right) \\
& & = & \left(\left( s | a \rightarrow 0\right) | b \rightarrow 1 \right) \\
& & = & \left( s | a \rightarrow 0, b \rightarrow 1 \right) \\
\end{eqnarray}
\begin{eqnarray}
\forall s \in S & \left[\!| P_2 |\!\right]_s & = & \left(\left( s | b \rightarrow 1 \right) | a \rightarrow 0\right) \\
& & = & \left( s | a \rightarrow 0, b \rightarrow 1 \right) \\
\end{eqnarray}
Donc, \left[\!| P_1 |\!\right] = \left[\!| P_2 |\!\right]
==== Grande Parenthèse ====
La sémantique dénotationnelle est une des approches qui permettent de formaliser un programme en utilisant les mathématiques. D'autres approches sont la __sémantique opérationnelle__, où un programme est vu comme un système de transitions d'états (dont nous dirons quelques mots), et la __sémantique axiomatique__, où un programme est vu comme une transformation de prédicats, et nous la développerons plus loin dans ce cours.
En sémantique dénotationnelle, on s'intéresse à l'effet du programme et pas à la manière de l'exécuter (ou dont c'est réalisé). Par exemple, \left[\!| P_1 |\!\right] = \left[\!| P_2 |\!\right], les deux programmes ont un même effet sur un état mémoire.
En sémantique opérationnelle, on s'intéresse à la manière don se font les calculs. La signification d'un programme est la suite des états mémoire de la machine qui exécute le programme. Par exemple, nos programmes ont les sémantique opérationnelles :
* P1 : s; (s | a -> 0); (s | a -> 0, b -> 1)
* P2 : s; (s | b -> 1); (s | a -> 0, b -> 1)
deux sémantiques différentes.
^ Remarques ^
| P1 et P2 ne sont pas opérationnellement équivalentes, mais deux programmes qui ne sont pas opérationnellement équivalentes peuvent aboutir au même état final. |
| Ces trois sémantiques (dénotationnelle, opérationnelle, axiomatique) ne sont pas complètement indépendente les unes des autres. \\ * 2 programmes syntaxiquement équivalentes le sont opérationnellement,\\ * 2 programmes opérationnellement équivalentes le sont dénotationnellement, \\ * deux programmes dénotationnellement équivalentes le sont axiomatiquement;\\ **mais les réciproques sont fausses.** |
==== fin Grande parenthèse ====
Suite des dénotations de nos instructions :
* conditionnelle : \left[\!| if\;b\;then\;A |\!\right]\left(s\right) =
* \left[\!| A |\!\right]\left(s\right) si \left[\!| b |\!\right]_{s}=\text{vrai}
* s si \left[\!| b |\!\right]_{s}=\text{faux}
* alternative | \left[\!| if\;b\;then\;A\;else\; B |\!\right]\left(s\right) =
* \left[\!| A |\!\right]\left(s\right) si \left[\!| b |\!\right]_{s}=\text{vrai}
* \left[\!| B |\!\right]\left(s\right) si \left[\!| b |\!\right]_{s}=\text{faux}
* répétition : \forall s\in S,\; \left[\!| \text{do } n \text{ times }A |\!\right]\left(s\right) = \underbrace{\left[\:| A |\!\right]\left(\left[\:| A |\!\right]\left(\ldots \left( \left[\:| A |\!\right]\left(s\right)\right)\right)\right)}_{\left[\!|n|\!\right]_s = x} = \left[\!| A |\!\right]^{\left[\!|n|\!\right]_s}\left(s\right)
* où \left[\!| A |\!\right]^{0}\left(s\right) = s
* et \left[\!| A |\!\right]^{i+1}\left(s\right) = \left[\!| A |\!\right]^{i}\left(\left[\!| A |\!\right]\left(s\right)\right),\quad i\in\mathbb{N}
* itération : \left[\!| \text{while } b \text{ do } A |\!\right] = \left[\!| \text{if } b \text{ then } \left\{A; \text{while } b \text{ do } A\right\} |\!\right]\left(s\right) mais ceci n'est pas compositionnelle : \left[\!| while |\!\right] ne dépend pas seulement de \left[\!| b |\!\right] et \left[\!| A |\!\right] mais aussi de \left[\!| while |\!\right] . Donc il faut trouver une autre définition qui soit compositionnelle.
* On peut remarquer que \left[\!| \text{while true do A} |\!\right]\left(s\right) n'est pas défini. La raison est qu'il n'y a aucun état mémoire atteignable par l'exécution de cette instruction. Ainsi, la sémantique de l'itération est une fonction **partielle** sur S, c'est à dire qui n'est définie que sur un sous-ensemble des états mémoire.
* Afin de définir la sémantique de l'itération, on ajoute à notre langage "L" une instruction fictive "bottom" notée = \bot **dont la sémantique est "__nulle part définie__" **. On va définir la sémantique d'itération comme la limite d'une suite croissante de fonctions partielles, chacune de ces fonctions étant la sémantique d'un programme. On considère la suite des programmes \left(W_i\right)_{i\in\mathbb{N}} définis par
* W_0 = \bot
* W_{i+1} = \text{if b then}\left\{ A; W_i \right\}, i\in\mathbb{N}
* La sémantique de ces programmes forme une suite croissante de fonctions partielles, au sens suivant, en notant w_i = \left[\!| W_i |\!\right]\quad \forall i\in\mathbb{N}
* dom\left(w_i\right) \subseteq dom\left(w_{i+1}\right)
* w_{i+1} |_{dom\left(w_{i}\right)} = w_i
* On peut alors définir une fonction w, limite de la suite. Par définition, \left[\!| \text{while } b \text{ do } A |\!\right] = w
=== Etude de la suite des programmes w ===
* w_0 = \left[\!| W_0 |\!\right] = \bot
* w_1 = \left[\!| W_1 |\!\right] définie par \forall s\in S, w_1\left(s\right) = \left[\!| \text{if b then A};\bot |\!\right]\left(s\right). \forall s\in S
* w_1\left(s\right) = \text{non definie} si \left[\!| b |\!\right]_{s} = vrai
* w_1\left(s\right) = s si \left[\!| b |\!\right]_{s} = faux
* w_2 = \left[\!| W_2 |\!\right] définie par \forall s\in S, w_1\left(s\right) = \left[\!| \text{if b then }\left\{A;W_1\right\} |\!\right]\left(s\right). \forall s\in S
* non définie si \left[\!| b |\!\right]_{s} = vrai et \left[\!| b |\!\right]_{\left[\!| A |\!\right]\left(s\right)} = vrai
* \left[\!| A |\!\right]\left(s\right) si \left[\!| b -\!\right]_{s} = vrai et \left[\!| b |\!\right]_{\left[\!| A |\!\right]\left(s\right)} = faux
* s autrement
* w_3 = \left[\!| W_3 |\!\right] définie par \forall s\in S, w_1\left(s\right) = \left[\!| \text{if b then } \left\{A;W_2 \right\} |\!\right]\left(s\right). \forall s\in S
* non définie si \left[\!| b |\!\right]_{ \left[\!| A |\!\right]\left(s\right)} = vrai et \left[\!| b |\!\right]_{\left[\!| A |\!\right]^{2}\left(s\right)} = vrai
* \left[\!| A |\!\right]^{2}\left(s\right) si \left[\!| b |\!\right]_{ \left[\!| A |\!\right]\left(s\right)} = vrai et \left[\!| b |\!\right]_{\left[\!| A |\!\right]^{2}\left(s\right)} = faux
* \left[\!| A |\!\right]\left(s\right) si \left[\!| b |\!\right]_{ s} = vrai et \left[\!| b -\!\right]_{\left[\!| A |\!\right]\left(s\right)} = faux
* s si \left[\!| b |\!\right]_{ s} = faux
* w_{i+1} = \left[\!| W_{i+1} |\!\right]= \left[\!| \text{ if b then }\left\{A;W_{i}\right\} |\!\right]\left( s \right) =
* non-définie si \left[\!| b |\!\right] = vrai ∧ \left[\!| b |\!\right]_{\left[\!| A |\!\right]\left(s\right)} = vrai ∧ ... ∧ \left[\!| b |\!\right]_{\left[\!| A |\!\right]^{i}\left(s\right)} = vrai
* \left[\!| A|\!\right]^{i}\left(s\right) si \left[\!| b |\!\right] = vrai ∧ \left[\!| b |\!\right]_{\left[\!| A |\!\right]\left(s\right)} = vrai ∧ ... ∧ \left[\!| b |\!\right]_{\left[\!| A |\!\right]^{i-1}\left(s\right)} = vrai ∧ \left[\!| b -\!\right]_{\left[\!| A |\!\right]^{i}\left(s\right)} = faux
* ...
* \left[\!| A|\!\right]\left(s\right) si \left[\!| b |\!\right] = vrai ∧ \left[\!| b |\!\right]_{\left[\!| A |\!\right]\left(s\right)} = vrai ∧ \left[\!| b |\!\right]_{\left[\!| A |\!\right]\left(s\right)} = faux
* s si \left[\!| b |\!\right]_{ s} = faux
Ainsi, on observe que généralement w_{i+1}\left( s \right) = w_{i}\left(\left[\!| A |\!\right] \left( s \right) \right) si \left[\!| b |\!\right] = vrai, et s si \left[\!| b |\!\right] = faux. Lorsqu'on passe i → ∞,
| w_{\infty}\left( s \right) = w_{\infty}\left(\left[\!| A |\!\right] \left( s \right) \right) | si \left[\!| b |\!\right] = vrai |
| s | si \left[\!| b |\!\right] = faux. |
De là on conclut que
* \left[\!| \text{while b do A} |\!\right]_{s} = \left[\!| \text{if b then} \left\{ A;\text{while b do A}\right\} |\!\right]\left( s \right)
qui est une propriété que l'on démontre à partir de la définition sémantique de l'itération.
[[semantics_4| ]] : Exemples de détermination de la sémantique de programmes par la construction de la suite de programmes.