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 (Wi) et leur fonction sémantique (wi)
i+1 | Wi+1 = | 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 |
wi+1(s) = non-définie si \left[\!| n |\!\right]_s > i et (s| n→ 0) si \left[\!| n |\!\right]_s \leq i
La limite de cette suite (wi) est la fonction définie par w(s) = (s | n→ 0). Donc le programme est équivalent à n:=0
.
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.
\left[\!| k:=0, x:=0 |\!\right]\left(s\right) = \left(s|_{x\rightarrow 0, k\rightarrow 0}\right)
Une itération de la boucle :
\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}
La limite de cette suite (wi) est la fonction w définie par
si \left[\!|k |\!\right]_{s} < \left[\!|n |\!\right]_{s} : 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)
si \left[\!|k |\!\right]_{s} \geq \left[\!|n |\!\right]_{s} : 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 \left[\!|n|\!\right]_s > 0
(s | k→0, x→0 ) si \left[\!|n|\!\right]_s = 0
semantics-4a ou Sémantique des Programmes Récursifs?