Probleme – D'autres règles d'inférence : prouver un programme

int s = 0;
int i = 1;
while (i <= n) { s = s + i; i = i + 1; }
/* on veut : s == n * (n + 1) / 2 */

1. Les règles. Elles s'écrivent exactement comme celles du chapitre — une barre, des prémisses au-dessus, une conclusion au-dessous.

$$\frac{}{\{Q[x\leftarrow E]\}x:=E\{Q\}}\text{aff}\frac{\{P\}{c}_1\{R\}\{R\}{c}_2\{Q\}}{\{P\}{c}_1;c_2\{Q\}}\text{seq}$$

$$\frac{\{I\wedge B\}c\{I\}}{\{I\}\text{while}B\text{do}c\{I\wedge \neg B\}}\text{boucle}\frac{P\Rightarrow P^{\prime }\{P^{\prime }\}c\{Q^{\prime }\}{Q}^{\prime }\Rightarrow Q}{\{P\}c\{Q\}}\text{conseˊq}$$

La règle de l'affectation se lit à l'envers, et c'est sa difficulté : pour que $Q$ soit vraie après $x:=E$, il faut que $Q$ où l'on a remplacé $x$ par $E$ soit vraie avant. Ainsi $\{s+i=f(i+1)\}s:=s+i\{s=f(i+1)\}$.

2. La correction partielle. On pose l'invariant

$$I:s=\frac{(i-1)i}{2}\wedge 1\le i\le n+1,$$

et le gardien $B:i\le n$. Trois pas.

Initialisation. Après s = 0; i = 1;, on a $s=0$ et $i=1$, donc $s=0=(1-1)\cdot 1/2$, et $1\le 1\le n+1$ dès que $n\ge 0$. L'invariant est établi. Formellement, deux applications de aff enchaînées par seq, puis conséq pour passer de la précondition $n\ge 0$ à la forme substituée.

Conservation. Il faut $\{I\wedge i\le n\}$ s = s + i; i = i + 1; $\{I\}$. En remontant depuis $I$ par la règle de l'affectation, appliquée deux fois de droite à gauche : Posons $\sigma (i)=\frac{(i-1)i}{2}$, de sorte que $\sigma (i+1)=\frac{i(i+1)}{2}$.

$$\mathcal{U}=\frac{}{\{s+i=\sigma (i+1)\}s:=s+i\{s=\sigma (i+1)\}}\text{aff}$$

$$\mathcal{V}=\frac{}{\{s=\sigma (i+1)\}i:=i+1\{s=\sigma (i)\}}\text{aff}$$

\dfrac{\mathcal{U} \qquad \mathcal{V}}% {\{s + i = \sigma(i{+}1)\}\ s := s{+}i\,;\ i := i{+}1\ \{s = \sigma(i)\}}\ \textsf{seq}

Il reste à vérifier $I\wedge i\le n\Rightarrow s+i=i(i+1)/2$, qui est de l'arithmétique : $s=(i-1)i/2$ donne $s+i=(i-1)i/2+i=i(i+1)/2$. Et la borne $i\le n$ assure $i+1\le n+1$. Une application de conséq conclut.

Sortie. La règle boucle donne $\{I\wedge \neg B\}$, c'est-à-dire $I$ et $i>n$. Avec $i\le n+1$ de l'invariant, on obtient $i=n+1$, d'où

$$s=\frac{(i-1)i}{2}=\frac{n(n+1)}{2}.$$

Le programme a été compilé et exécuté avec ces trois assertions posées dans le code, pour $n=0$ à $200$ : les $201$ cas passent, et $\text{somme}(100)=5050$.

3. La correction totale demande la terminaison, que la logique de Hoare ci-dessus ne donne pas : la règle boucle suppose qu'on sorte. On ajoute un variant : l'entier $n+1-i$. Il est positif tant que le gardien tient ($i\le n$ donne $n+1-i\ge 1$), et il décroît strictement de $1$ à chaque tour puisque $i$ croît de $1$. Une suite d'entiers positifs strictement décroissante est finie : la boucle fait exactement $\max (n,0)$ tours.

4. Ce qui est identique, et ce qui diffère.

Identique : la forme. Des règles à prémisses et conclusion, des dérivations qui sont des arbres, une lecture de bas en haut guidée par la forme du but, et une preuve de correction par induction sur la dérivation. Tout le vocabulaire du chapitre s'applique tel quel — et c'est ce que le programme entend par « d'autres utilisations de règles d'inférence pour raisonner ».

Différent : les objets. Les séquents du chapitre relient des formules entre elles ; les triplets relient une formule, un programme et une formule. Et surtout, la règle conséq contient deux implications $P\Rightarrow P^{\prime }$ et $Q^{\prime }\Rightarrow Q$ qui ne sont pas démontrées par ce système-ci : ce sont des énoncés d'arithmétique, renvoyés à une autre théorie. La logique de Hoare n'est pas close sur elle-même, là où la déduction naturelle propositionnelle l'est.

Ce que ce problème referme. Le chapitre chap:algo-prog demandait, pour chaque algorithme, une spécification, un invariant, un variant et une complexité. On voit ici que ces quatre exigences ne sont pas une convention de rédaction : l'invariant est la prémisse de la règle boucle, le variant est ce qui manque à cette règle pour donner la terminaison, et la spécification est le triplet lui-même. Le formalisme que le chapitre 3 imposait sans le nommer est celui-ci.