
\Exercice{Somme des carrés des $N$ premiers entiers pairs}

\begin{code}[frame=single, label = {\sc programme}, numbers=left]
 x:=0 ; k:= 0 ; i:=0 ;
 while(i < N){ 
   i:= i + 1 ; 
   k:= k + 2 ;
   x:= x + k * k  ; 
}
\end{code}


\Question{\Bareme{1}}
Dessinez l'automate correspondant au programme précédent.

\begin{Math}
q_0  \Fr{\answer{x\:=0 ~;~ k\:=0 ~;~ i\:=0}}   q_1
\\
q_1 \Fr{\answer{i \geq N}} q_s
\\
q_1 \Fr{\answer{i < N}} q_2 
\\
q_2 \Fr{\answer{i\:=~i+1~~}} q_3
\\
q_3 \Fr{\answer{k\:=~k + 2~~}} q_4
\\
q_4 \Fr{\answer{x\:=x+k\*k}} q_1
\end{Math}

\Question{\Bareme{1}}
Faîtes quelques exécutions pour trouver l'égalité qui relie les variables \PRG{k} et \PRG{i}.


\Question{\Bareme{8}} 
Montrez par la technique de Floyd-Dijkstra-Hoare que
l'état de sortie du programme précédent vérifie la propriété
\begin{math}
x = \frac{2N(N+1)(2N+1)}{3}
\end{math}

\begin{corrige}
\begin{solution}
\def\EQ#1{\frac{2 #1 (#1+1)(2#1+1)}{3}}
\begin{Math}
\psi_s \defas x = \EQ{N}
\\
\psi_1 \defas i\leq N \andl x = \EQ{i} \andl k=2i
\\
\psi_4 \defas \psi_1[x \:= x+k^2] \equiv i\leq N  \andl x + k^2 = \EQ{i} \andl k=2i
\\
\psi_3 \defas \psi_4[k \:= k+2] \equiv i\leq N \andl x+(k+2)^2 = \EQ{i} \andl k+2 = 2i
\\
\psi_2 \defas \psi_3[i\:=i+1] \equiv i+1 \leq N \andl x+(k+2)^2 = \EQ{(i+1)} \andl k+2 = 2(i+1)
\\
\psi_0 \defas \psi_1[x\:=0 ; k\:=0 ; i\:=0] \equiv 0 \leq N \andl 0 = \EQ{(0)} \andl 2 = 2\* 0 \equiv 0 \leq N
\end{Math} 

Vérification des invariants:

\begin{Math}
\Overbrace{i\leq N \andl \Underbrace{x = \EQ{i}}{A} \andl \Underbrace{k=2i}{B}}{\psi_1} 
\andl 
\Overbrace{i<N}{test} 
\\
\isit{\impL} 
\\
\Overbrace{\Underbrace{i+1 \leq N}{test} \andl \Underbrace{x+(k+2)^2 = \EQ{(i+1)}}{d'apres~A~\andl~B} \andl \Underbrace{k+2 = 2(i+1)}{B}}{\psi_2}
\end{Math}
\end{solution}
\end{corrige}


\Question{\Bareme{1}} 
En déduire les conditions intiales du programme qui garantissent la propriété 
de correction à l'état de sortie.


\clearpage


\Exercice{Somme des carrés des $K$ premiers entiers impairs}

\begin{code}[frame=single, label = {\sc programme}, numbers=left]
 r:=0 ; u:= 1 ; j:=0 ;
 while(j < K){ 
   r:= r + u * u  ; 
   j:= j + 1 ;
   u:= u + 2 ;
}
\end{code}


\Question{\Bareme{1}}
Dessinez l'automate correspondant au programme précédent.

\begin{Math}
q_0  \Fr{\answer{r\:=0 ~;~ u:=1 ~;~ j\:=0}}   q_1
\\
q_1 \Fr{\answer{j \geq K}} q_s
\\
q_1 \Fr{\answer{j < K}} q_2 
\\
q_2 \Fr{\answer{r\:=r+u\*u}} q_3
\\
q_3 \Fr{\answer{j\:=~j+1~~}} q_4
\\
q_4 \Fr{\answer{u\:=~u+2~~}} q_1
\\
\end{Math}

\Question{\Bareme{1}}
Faîtes quelques exécutions pour trouver l'égalité qui relie les variables \PRG{u} et \PRG{j}.


\Question{\Bareme{8}} 
Montrez par la technique de Floyd-Dijkstra-Hoare que
l'état de sortie du programme précédent vérifie la propriété
\begin{math}
r = \frac{K(2K-1)(2K+1)}{3}
\end{math}


\begin{corrige}
\begin{solution}
\def\EQ#1{\frac{#1(2#1-1)(2#1+1)}{3}}
\begin{Math}
\psi_s \defas r = \EQ{K}
\\
\psi_1 \defas j\leq K \andl r = \EQ{j} \andl u=2j+1
\\
\psi_4 \defas \psi_1[u \:= u+2] \equiv j\leq K \andl r = \EQ{j} \andl u+2=2j+1
\\
\psi_3 \defas \psi_4[j \:= j+1] \equiv j+1\leq K \andl r = \EQ{j+1} \andl u+2=2(j+1)+1
\\
\psi_2 \defas \psi_3[r\:=r+u^2] \equiv j+1\leq K \andl r + u^2 = \EQ{j+1} \andl u=2j+1
\\
\psi_0 \defas \psi_1[r\:=0 ; u\:=1 ; j\:=0] \equiv 0\leq K \andl 0 = \EQ{(0)} \andl 1=2\*0+1 \equiv 0 \leq K
\end{Math} 

Vérification des invariants:

\begin{Math}
\Overbrace{j\leq K \andl \Underbrace{r = \EQ{j}}{A} \andl \Underbrace{u=2j+1}{B}}{\psi_1} 
\andl 
\Overbrace{j<K}{test} 
\\
\isit{\impL} 
\\
\Overbrace{\Underbrace{j+1\leq K}{test} \andl \Underbrace{r + u^2 = \EQ{j+1}}{d'apres~A~\andl~B} \andl \Underbrace{u=2j+1}{B}}{\psi_2}
\end{Math}
\end{solution}
\end{corrige}


\Question{\Bareme{1}} 
En déduire les conditions intiales du programme qui garantissent la propriété 
de correction à l'état de sortie.



\endinput

\Exercice{Somme des carrés des $N$ premiers entiers}

\begin{code}[frame=single, label = {\sc programme}, numbers=left]
 r:=0 ; i:=0 ;
 while(i < N){ 
   i:=i+1 ;
   r:=r+i*i ; 
}
\end{code}



\Question{\Bareme{1}}
Dessinez l'automate correspondant au programme précédent.


\begin{Math}
q_0  \Fr{\answer{r\:=0 ~;~ i\:=0}}   q_1
\\
q_1 \Fr{\answer{i \geq N}} q_s
\\
q_1 \Fr{\answer{i < N}} q_2 
\\
q_2 \Fr{\answer{i\:=~i+1~~}} q_3
\\
q_3 \Fr{\answer{r\:=r+i\*i}} q_1
\\
\end{Math}



\Question{\Bareme{8}} 
Montrez par la technique de Floyd-Dijkstra-Hoare que
l'état de sortie du programme précédent vérifie la propriété
\begin{math}
r = \frac{N(N+1)(2N+1)}{6}
\end{math}


\begin{corrige}
\begin{solution}
\begin{Math}
\psi_s \defas r = \frac{N(N+1)(2N+1)}{6} 
\end{Math}

On choisit $\psi_1$ afin de satisfaire l'implication
\begin{Math}
\psi_1 \andl i\geq N \impL \Overbrace{r = \frac{N(N+1)(2N+1)}{6} \andl i=N}{\psi_s}
\end{Math}

On prend 
\begin{math}
\psi_1 \defas r = \frac{i(i+1)(2i+1)}{6} \andl i\leq N
\end{math}

On a bien : 
\begin{Math}
\psi_1 \andl \Underbrace{i\geq N}{test} \impL r=\frac{i(i+1)(2i+1)}{6} \andl i=N
\textit{~~d'où~~} r = \frac{N(N+1)(2N+1)}{6} 
\end{Math}

La transition $q_3 \Fr{r\:=r+i\*i} q_1$ ne fait que des affectations donc le meilleur choix pour $\psi_3$ est 
\begin{Math}
\psi_3 \defas \psi_1 [r \:= r + i\*i]
\\
\psi_3 \equiv r + i^2 = \frac{i(i+1)(2i+1)}{6} \andl i \leq N
\end{Math}

La transition $q_2 \Fr{i\:=i+1} q_3$ ne fait que des affectations donc le meilleur choix pour $\psi_2$ est 
\begin{Math}
\psi_2 \defas \psi_3 [i \:= i+1]
\\
\psi_2 \equiv r + (i+1)^2 = \frac{(i+1)(i+1+1)(2(i+1)+1)}{6} \andl i+1 \leq N
\end{Math}

\paragraph{Étape de vérification}
Les propriétés $\psi_1$ et $\psi_2$ sont connues. 
La transition $q_1 \Fr{i < N} q_2$ nous permet de vérifier la cohérence de
propriétés choisies. Les propriétés $\psi_i$ sont des invariants si l'implication
suivante est satisfaite :
\begin{Math*}
(*)~~
\Overbrace{\Underbrace{r = \frac{i(i+1)(2i+1)}{6}}{A} \andl i\leq N}{\psi_1}
\andL 
\Overbrace{i < N}{test}
\isit{\impL}
\Overbrace{\Underbrace{r + (i+1)^2 = \frac{(i+1)(i+1+1)(2(i+1)+1)}{6}}{B} \andl \Underbrace{i+1 \leq N}{test}}{\psi_2}
\end{Math*}

Montrons qu'en fait 
\begin{math}
(A)~~r=\frac{i(i+1)(2i+1)}{6}
\end{math}
équivaut à 
\begin{math}
(B)~~r + (i+1)^2 = \frac{(i+1)(i+2)(2(i+1)+1)}{6}
\end{math}

Pour cela montrons que 
\begin{Math}[rcl]
\frac{(i+1)(i+2)(2(i+1)+1)}{6} - (i+1)^2 &\isit=& \frac{i(i+1)(2i+1)}{6}
\\
\ie.~~ (i+1)\textcolor{red}{(i+2)}(2i+3) - 6(i+1)^2 &\isit=& i(i+1)(2i+1) 
\end{Math}

Détails des calculs:
\begin{Math}[rcl]
(i+1)\textcolor{red}{(i+2)}(2i+3) - 6(i+1)^2
&=& \textcolor{red}{i}(i+1)\textcolor{blue}{(2i+3)} \textcolor{red}{+ 2}(i+1)(2i+3) - 6(i+1)^2
\\&=& i(i+1)(2i+\textcolor{blue}{1}) + \textcolor{blue}{2}i(i+1) + 2(i+1)(2i+3) - 6(i+1)^2
\\&=& i(i+1)(2i+1) +  \overbrace{(i+1)(\underbrace{2i + 2(2i+3) -6(i+1)})}
\\&=& i(i+1)(2i+1) + ~~~~~~~~~~~~~~~~~~~~~~~~ 0 
\\&\holds{=}& i(i+1)(2i+1) 
\end{Math}\cqfd

L'implication $(*)$ est satisfaite ce qui termine la preuve que les propriétés $\psi_i$ sont des invariants d'états.
\end{solution}
\end{corrige}



\Question{\Bareme{2}}
Donnez les conditions d'utilisations du programme. Et conclure quant à la correction du programme (terminaison et correction partielle).

\begin{corrige}
\begin{solution}
Les conditions d'utilisations correspondent à la propriété de l'état initial $q_0$.

La transition $q_0 \Fr{r\:=0 ; i\:=0} q_1$ ne fait que des affectations donc le meilleur choix pour $\psi_0$
est :
\begin{Math}
\psi_0 \defas \psi_1 [ r\:=0 ; \i:=0]
\\
\psi_0 \equiv 0 = \frac{0(0+1)(20+1)}{6} \andl 0 \leq N
\\ \equiv 0 = 0 \andl 0 \leq N
\\ \equiv 0 \leq N
\end{Math}

La correction partielle du programme est garantie pour toutes les valeurs de $N$ possibles.
La terminaison en revanche n'est garantie que pour $N\geq -1$.
\end{solution}
\end{corrige}
