\section{Logique de Hoare}

\def\hoare#1#2#3{#1\stackrel{#2}\longrightarrow#3}
\def\Hoare#1#2#3{\{#1\}#2\{#3\}}
\def\IFT#1#2#3{(#1)?#2:#3}
\def\WHILE#1#2{{\rm W}(#1)#2}

\subsection{formalisme}

La logique de Floyd-Hoare est une méthode de
preuve formelle décrite par Hoare en
1969. Elle étend la logique des prédicats
par l'ajout d'un nouveau symbole :
$$
\hoare pSq, \qquad\text{souvent noté}\quad\Hoare pSq
$$
ou $p$ (précondition) , $q$ (postcondition)  
sont des prédicats logiques et $S$ un
programme (action). Le symbole $\hoare pSq$ généralise l'implication
logique, il se lit : $p$ par le programme $S$ entraine $q$. Tout
le monde peux se convaincre que :

$$
\hoare{x=\alpha}{\begin{substack}x:=x+y;\\y:=x-y;\\x=x-y\end{substack}}{x=\beta}
$$

Il suffit de tracer la séquence d'affectation \voir{SWAP}.

\begin{table}
\caption{\label{SWAP}Traçage d'une séquence d'affectation.}
\begin{tabular}{ccl}
x    &y              &\\
\hline
$\alpha$         &$\beta$   &\\
                 && x:= x+y  \\
$\alpha+\beta$   &$\beta$   &\\
                 && y:= x-y  \\
$\alpha+\beta$   &$\alpha$   &\\
                 && x:= x-y  \\
$\beta$   &$\alpha$   &\\
\end{tabular}
\end{table}

La logique de Hoare permet de formaliser
ce type de preuve. On s'intéresse aux séquences 
de programme $S;P$, à l'affectation des variables $x:=t$, 
à l'alternative $\IFT cST$ et l'itération 
$\WHILE bS$. 

\subsection{règle}
\subsection{quelques preuves}
\subsection{exercice}

