\begin{local}
% --- macros
\newcommand\Spar[1]{\,{\small(}#1{\small)}\,} 
\newcommand\Tpar[1]{\,{\scriptstyle(}#1{\scriptstyle)}\,} 
% --- macros


\Exercice{Calcul des termes de la suite de Fibonacci -- version avec seulement deux variables \Bareme{9}}

\begin{code}
 i:=N-1 ; x:=1; y:=1 ;
 while(i<>0){ y:=y+x ; x:=y-x ; i:=i-1; }
\end{code}

On prétend qu'à la sortie du programme le résultat $y$ satisfait la propriété
\begin{math}
 y = fib(N)
\end{math}
où 
\begin{System}
fib(0) = 1
\\
fib(1) = 1
\\
fib(n+1) = fib(n) + fib(n-1)
\end{System}



\Question{\Bareme{1}}
%
Donnez les transitions de l'automate correspondant au programme ci-dessus 
($q_0$ représente le point d'entrée et $q_s$ celui de sortie de l'automate).
%
\begin{Math*}
q_1 \Fr{\answer{i=0}} q_s
\\
q_0 \Fr{\answer{i:=N-1;x:=1;y:=1;}} q_1
\\
q_1 \Fr{\answer{i\neq 0}} q_2
~~~~
q_2 \Fr{\answer{y} ~:=~ \answer{x+y}} q_3
~~~~
q_3 \Fr{\answer{x} ~:=~ \answer{y-x}} q_4
~~~~
q_4 \Fr{\answer{i} ~:=~ \answer{i-1}} q_1
\end{Math*}





\Question{\Bareme{4} \textbf{Preuve de correction partielle}}
%
Rédigez la preuve (en suivant la méthode de Floyd-Dijsktra-Hoare)
qu'à la sortie du programme $y=fib(N)$.
%
La qualité et la précision de la rédaction compte pour une grande part dans la note.
%
Vous prendrez pour invariant en $q_1$
une propriété de la forme :
\begin{Math*}[r]
y= \answer{fib(N-i)} \andl \answer{~x~}=fib(\answer{N-i}-k)  
\\[2ex]
\textit{où k est une constante que vous devrez déterminer}
\end{Math*}

\begin{corrige}
\begin{solution}
\begin{enumerate}
\item Transition $q_1 \Fr{\answer{i:=0}} q_s$
%
\begin{Math}
\psi_1 \andl i=0 \impL \Overbrace{y=fib(N)}{\psi_s}
\end{Math}
%
On choisit $\psi_1 \defas y=fib(N-i) \andl x=fib(N-i-k)$

Lorsque $i=0$, $\psi_1$ nous donne $y=fib(N)$  (et d'autres propriétés qui ne sont pas utiles pour $\psi_s$).

\item Transition $q_4 \Fr{i:=i-1} q_1$
\begin{Math}[rcl]
\psi_4 &\defas& \psi_1[i:=i-1] 
\\
&\defas& y = fib(N-(i-1)) \andl x = fib(N-(i-1)-k)
\\
&\equiv& y = fib(\Tpar{N-i}+1) \andl x=fib(\Tpar{N-i}+1-k)
\end{Math}

\item Transition $q_3 \Fr{x:=y-x} q_4$
\begin{Math}[rcl]
\psi_3 &\defas& \psi_4[x\:=y-x] 
\\
&\defas& y = fib(\Tpar{N-i}+1) \andl y-x=fib(\Tpar{N-i}+1-k)
\end{Math}

\item Transition $q_2 \Fr{y:=x+y} q_3$
\begin{Math}[rcl]
\psi_2 &\defas& \psi_3[y\:=x+y] 
\\
&\defas& x+y = fib(\Tpar{N-i}+1) \andl (x+y)-x=fib(\Tpar{N-i}+1-k)
\\
&\equiv& x+y = fib(\Tpar{N-i}+1) \andl y=fib(\Tpar{N-i}+1-k)
\end{Math}

\item Transition $q_1 \Fr{i\neq 0} q_2$ \textsc{Vérification des invariants choisis}
%
Il s'agit de vérifier que limplication suivante est valide.
%
\begin{Math}
\Overbrace{y=fib(N-i) \andl x=fib(\Tpar{N-i}-k)}{\psi_1}
\andl 
\Overbrace{i\neq N}{garde}
\\
\isit{\impL} 
  \Overbrace{\Underbrace{x+y\isit{=}fib(\Tpar{N-i}+1)}{(**)} 
  ~\andl~ 
  \Underbrace{y\isit{=}fib(\Tpar{N-i}+1-k)}{(*)}}{\psi_2}
\end{Math}

\begin{itemize}
\item[$(*)$] Si on choisit $k=1$ alors $(*)$ devient
  $y\isit{=}fib(\Tpar{N-i}$ et c'est alors le premier terme de la
  prémisse de l'implication, donc cette partie de la conclusion de l'implication est trivialement démontrée.

\item[$(**)$]
En prenant $k=1$ on a alors en prémisse de l'implication
$y=fib(N-i)$ et $x=fib((N-i)-1)$, 
on peut remplacer $x$ et $y$ par leurs valeurs dans le terme $(**)$ qui devient alors
\begin{math*}
  fib(N-i)+fib((N-i)-1)\isit{=}fib((N-i)+1)
\end{math*}
% 
Cette égalité valide d'après la définition du $n\eme$ terme de la suite de Fibonacci avec $n=N-i$
\end{itemize}
\end{enumerate}
\end{solution}
\end{corrige}



\Question{\Bareme{2}}
%
Récapitulez les invariants 
\begin{Math}
 \psi_1 \defas
 \\[3ex]
 \psi_2 \defas
 \\[3ex]
 \psi3 \defas
 \\[3ex]
 \psi4 \defas
\end{Math}



\Question{\Bareme{1}}
%
En déduire les conditions d'utilisation du programme. Détaillez vos étapes de calcul et de simplification.
%
\begin{corrige}
\begin{solution}
Transition $q_0 \Fr{i:=N-1; x:=1 ; y:=1} q_1$
\begin{Math}[rcl]
\psi_0 &\defas& \psi_1[i\:=N-1; x\:=1; y\:=1]
\\
&\equiv& \PAR{y=fib(N-i) \andl x=fib(N-i-1)}[i\:=N-1; x\:=1; y\:=1]
\\
&\equiv& \PAR{1=fib(N-\Tpar{N-1}) \andl 1=fib(N-\Tpar{N-1}-1)}
\\
&\equiv& \Underbrace{1=fib(1)}{vrai} \andl \Underbrace{1=fib(0)}{\vrai} 
\\
&\equiv& \textit{vrai par définition de la suite de Fibonacci}
\end{Math}
\end{solution}
\end{corrige}


\Question{\Bareme{1}}
%
Comment se comporte le programme pour $N=0$ ?
%
Expliquez pourquoi la condition $N>0$ n'apparaît pas comme condition d'utilisation du programme ?

\end{local}

