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 (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.

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.

\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}

  • Wi+1 = 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
  • wi+1 = non-définie si \left[\!|k |\!\right]_{s} < \left[\!|n |\!\right]_{s} - i
    • = ( s | k→s(n), x→s(x)+(s(k)+s(k)+1+s(k)+2…+s(k)+s(n)) ) si \left[\!|k |\!\right]_{s} = \left[\!|n |\!\right]_{s} - i
    • = ( s | k→s(n), x→s(x)+s(n)) si \left[\!|k |\!\right]_{s} = \left[\!|n |\!\right]_{s} - 1

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?


 
m1ilc/semantics_4.txt · Dernière modification: 2010/05/24 08:01 par suitable