==== Détermination de la sémantique de Programmes ====

=== Exercice 1 ===

Déterminer la sémantique du programme

  while n > 0 do
    n := n-1
    
pour n∈N.

Pour cela, on construit la suite des programmes (W<sub>i</sub>) et leur fonction sémantique (w<sub>i</sub>)

^ i+1 | W<sub>i+1</sub> = | if n>0 then   |
^ i  |                   |  { n:= n-1;  if n>0 then {  |
^ i-1 |           |  { n:= n-1;  if n>0 then {  |
^ ... |  |  |
^  0 |  |  { n:= n-1; bottom }... }}}}}  | avec i accolades fermantes |

w<sub>i+1</sub>(s)  = non-définie si <jsm>\left[\!| n |\!\right]_s > i</jsm> et (s| n-> 0) si <jsm>\left[\!| n |\!\right]_s \leq i</jsm>

La limite de cette suite (w<sub>i</sub>) est la fonction définie par w(s) = (s | n-> 0). Donc le programme est équivalent à ''n:=0''.


=== Exercice 2 ===

Déterminer la sémantique due programme

  k := 0; x := 0;
  while k < n do {
    k := k+1; x:= x + k;
    }
    
Procédons en deux temps, la sémantique des premières affectations, puis du corps de l'itération.

<jsm>\left[\!| k:=0, x:=0 |\!\right]\left(s\right) = \left(s|_{x\rightarrow 0, k\rightarrow 0}\right)</jsm>

Une itération de la boucle :

<jsmath>
\begin{eqnarray}
\left[\!| k:=k+1; x:=x+k |\!\right] & = & \left[\!| x:=x+k |\!\right]\left( \left[\!| k = k+1 |\!\right] \left(s\right)\right) \\
 & = & \left[\!| x:=x+k |\!\right]\left(s\prime|_{k\rightarrow s\left(k \right)+1}\right) \\ 
 & = & \left(s\prime | k\rightarrow s\left(k\right)+1, x\rightarrow s\left(x\right)+s\left(k\right) +1\right)\\
\left[\!| k:=k+1; x:=x+k |\!\right]^{i}\left(s\right) & = & \left(s | k\rightarrow s\left(k\right)+i, x\rightarrow s\left(x\right)+\left(s\left(k\right)+1\right)+\left(s\left(k\right)+2\right)+\ldots +\left(s\left(k\right)+i\right)\right)
\end{eqnarray}
</jsmath>

  *  W<sub>i+1</sub>  =  if k<n then
    * {k:=k+1;x:=x+k; if k<n then
      * {k:=k+1;x:=x+k; if k<n then
        * {k:=k+1;x:=x+k; if k<n then
        * ... i-3 imbrications de plus, puis
        * {k:=k+1;x:=x+k; bottom}
    * }}} <- i accolades 


  * w<sub>i+1</sub> = non-définie si <jsm>\left[\!|k |\!\right]_{s} < \left[\!|n |\!\right]_{s} - i </jsm>
    * = ( s | k->s(n), x->s(x)+(s(k)+s(k)+1+s(k)+2...+s(k)+s(n)) ) si <jsm>\left[\!|k |\!\right]_{s} = \left[\!|n |\!\right]_{s} - i </jsm>
    * = ( s | k->s(n), x->s(x)+s(n)) si <jsm>\left[\!|k |\!\right]_{s} = \left[\!|n |\!\right]_{s} - 1</jsm>

La limite de cette suite (w<sub>i</sub>) est la fonction w définie par
  * si <jsm>\left[\!|k |\!\right]_{s} < \left[\!|n |\!\right]_{s} </jsm> : <jsm>w\left(s\right) = \left( s | k\rightarrow s\left(n\right), x\rightarrow s\left(x\right)+s\left(k\right)+\left(s\left(k\right)+1\right)+\left(s\left(k\right)+2\right)+\ldots + s\left(n\right)\right)</jsm>
  * si <jsm>\left[\!|k |\!\right]_{s} \geq \left[\!|n |\!\right]_{s} </jsm> : s

Appliquée à l'état (s | k->0, x->0) on obtient l'état final : 
  * (s|k->s(n), x->1+2+...s(n)) si <jsm>\left[\!|n|\!\right]_s > 0</jsm>
  * (s | k->0, x->0 ) si <jsm>\left[\!|n|\!\right]_s = 0</jsm>

----
[[semantics-4a|]] ou [[semantics_5|]]?