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_i) et leur fonction sémantique (w_i)

w_i+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 (w_i) 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 :

• W_i+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

• w_i+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 (w_i) 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?