Sémantique opérationnelle

Pour pouvoir décrire par une formule de logique ce que fait un programme il faut d'abord donner une signification à ce que fait un programme. Pour cela on va définir un peu plus formellement le comportement d'un programme: on va définir une sémantique opérationnelle.

On peut (avec difficulté) définir une sémantique opérationnelle pour un langage de programmation. Considérons que l'état du système ( $S \in \mathcal{S}$) est décrit par l'état des variables du système: ( $S \in [Var \rightarrow V]$), il est relativement facile de définir l'effet des diverses instructions sur cet état du système. On notera $S(v)$ la valeur de $v$ dans l'état $S$.

Par exemple:

• si $I$ est une affectation: x:=e où $e$ est une expression. $e$ peut être évaluée dans n'importe quel état $S$:
  • si $e=c$ où $c$ est une constante $\mathcal{E}(S)(e)=c$
  • si $e=v$ où $v$ est une variable $\mathcal{E}(S)(e)=S(v)$
  • si $e=e_1+e_2$ alors $\mathcal{E}(S)(e)=\mathcal{E}(S)(e_1)+\mathcal{E}(S)(e_2)$
  • ...
  Alors le nouvel état obtenu sera tel que dans cet état uniquement la valeur de x a été modifiée et vaut après cette affectation $\mathcal{E}(S)(e)$. On peut définir une substitution $[x \leftarrow v]$ par:
  • $S[x \leftarrow v](x')= S(x)$ si $x \neq x'$
  • $S[x \leftarrow v](x)= v$
  Dans ce cas, le nouvel état obtenu après avoir appliqué l'instruction x:=e à l'état $S$ sera $S'= S[x \leftarrow \mathcal{E}(S)(e)]$.

  On peut donc définir l'effet des instructions sur les états du système: $\mathcal{I}(\mathtt{Ins})$ est une fonction (partielle) de $\mathcal{S}$ dans $\mathcal{S}$. Par exemple, comme on vient de le voir:
  

  $$\forall S\in \mathcal{S}: \mathcal{I}(\mbox{\texttt{x:=e}})(S)=S[x\rightarrow e]$$
  
  

• Si I est $\mathtt{I_1;I_2}$ où $\mathtt{I_1}$ et $\mathtt{I_2}$ sont des instructions, si $S$ est l'état de départ, l'effet de $\mathtt{I_1;I_2}$ sera:
  
  $$\mathcal{I}(\mathtt{I_1;I_2})(S)=\mathcal{I}(I_2)(\mathcal{I}(I_1)(S))$$
  
  
  En d'autres termes, $\mathcal{I}(\mathtt{I_1;I_2})=\mathcal{I}(\mathtt{I_1})\circ\mathcal{I}(\mathtt{I_2})$.
• On peut de la même façon définir l'effet des autres instructions. La seule instruction qui pose problème est la boucle, car on ne peut pas toujours déterminer le nombre d'itérations et $\mathcal{I}$ ne sera pas défini pour tout $S$: si le programme boucle on notera l'état indéfini obtenu $\bot$. Si $\mathtt{Ins}$ boucle à partir de l'état $S$, on le notera donc: $\mathcal{I}(\mathtt{Ins})(S)=\bot$. Si on considère une boucle while $\mathtt{C}$ do $\mathtt{Ins}$ od. Si l'on a définit $\mathcal{I}(\mathtt{Ins})$ alors, pour tout état $S$, si $n$ est le plus petit entier s'il existe tel que $\mathcal{E}((\mathcal{I}(\mathtt{Ins}))^{n_S}(S))(C)=False$,¹ alors $\mathcal{I}(\mbox{\texttt{while} $\mathtt{C}$\ \texttt{do} $\mathtt{Ins}$\texttt{od}})(S)=(\mathcal{I}(\mathtt{Ins}))^{n_S}(S)$...

On peut donc définir l'effet des instructions sur les états du système: $\mathcal{I}(\mathtt{Ins})$ est une fonction (partielle) de $\mathcal{S}$ dans $\mathcal{S}$. Par exemple, comme on vient de le voir:

$$\forall S\in \mathcal{S}: \mathcal{I}(\mathtt{x:=e})(S)=S[x\rightarrow e]$$

Exercice: Définir $\mathcal{I}(\mathtt{x:=x+3+y})$. Si $S(x)=0$ et $S(y)=2$ quelle sera la valeur de $x$ dans le nouvel état.

Définir $\mathcal{I}$ pour une instruction if then else.

Vérifier que while C do I od est équivalent à if C then I; while C do I od fi

Ce résultat peut servir à définir $\mathcal{I}(\mbox{\texttt{while C do I od}})$:

Soit $\mathcal{H}(F)$ (où $F$ est une fonction de l'ensemble des états dans l'ensemble de états) défini pour chaque état $S$ par:

$$\mathcal{H}(F)(S)= \mbox{ if } \mathcal{E}(C)(S) \mbox{ then } (\mathcal{H}(F))(\mathcal{I}(I)(S)) \mbox{ else } S$$

On peut vérifier que: $\mathcal{H}(\mathcal{I}(\mbox{\texttt{while C do I od}}))=\mathcal{I}(\mbox{\texttt{while C do I od}})$ et donc que $\mathcal{I}(\mbox{\texttt{while C do I od}}))$ est une point fixe de $\mathcal{H}$ (i.e. une fonction $F$ telle que $\mathcal{H}(F)=F$)