I. Exercice 1

Demontrer que :
{n > 0}
i := 1;
k := 0;
while 2*i <= n do
begin
    i := 2*i;
    k := k+1;
end;
{2^k =< n < 2^(k+1)}

Nous savons que la partie la plus difficile de l'exercice residera dans l'identification de l'invariant de la boucle. Pour cela, la premiere chose a faire est de chercher intuitivement un invariant qui pourrait convenir. Pour trouver un invariant, il faut :
- une bonne idee
- verifier que l'invariant est vrai avant le debut de la boucle
- verifier que l'invariant et la negation de la condition de boucle permettent de deduire la post-condition
- regarder "intuitivement" si l'invariant demeure inchange a chaque tour de boucle (on le montre ensuite rigoureusement)

Pour demontrer une boucle, nous cherchons a appliquer la condition suffisante suivante :

Ou P est l'invariant, B la condition de la boucle et S la suite d'instructions. Ici, B correspond a 2*i <= n et S a  i := 2*i; k := k+1;

On cherche donc P tel que
{ P & 2*i <= n }  i := 2*i; k := k+1; { P }

Ici B n'est d'aucun secours pour trouver l'invariant. En revanche, on observe que k est un simple compteur du nombre de tour de boucle et qu'a chaque tour de boucle, i double d'ou l'idee d'essayer l'invariant i = 2^k.
Cette egalite est vraie pour les conditions initiales (1 = 2 ^ 0) et il semble qu'apres le dernier tour de boucle, on obtienne effectivement les inegalites de la post-condition (cela n'a rien d'evident donc nous y reviendrons plus rigoureusement).
On se propose maintenant de montrer que  { P & B } S { P }.
On observe que S est compose de plusieurs instructions qui sont des assignations, nous aurons donc a utiliser les deux regles suivantes :

Pour determiner P a partir de Q, il faut remplacer toutes les occurences de la variable v par l'expression e. Pour determiner Q a partir de P, on determine les consequences logiques de l'assignation (c'est moins clair car la determination de Q se fait au cas par cas suivant ce que l'on cherche a demontrer mais en general, c'est aussi plus facile a deviner).

{ P & B }
{ i = 2^k & 2*i <= n }

i := 2*i;

{i / 2 = 2^k & i <= n}    (d'apres (2))
{i = 2^(k+1)}                (on decide de laisser la condition i <= n car elle ne nous servira pas pour prouver { P })

k := k+1;

{i = 2^k}                        (d'apres (2))
{P}

Par (3), on obtient donc :
{ P & B }  i := 2*i; k := k+1; { P } soit { P & B } S { P }.

On sait que la boucle se termine car la fonction k -> 2^k est croissante et tend vers l'infini donc il existe forcement un entier k tel que
2^(k+1) = 2*i > n puisque n > 0 (et la boucle s'arrete pour le plus petit entier k verifiant cette inegalite, ce sera important par la suite).

Par (1), nous avons donc demontre :

{i = 2^k}
while 2*i <= n do
begin
    i := 2*i;
    k := k+1;
end;
{i = 2^k & 2*i > n}

Il reste a inclure cela dans la preuve globale (mais le plus dur est fait !) :

{n > 0}
{n > 0 & 1 = 1}        (tres formellement pour que la demonstration soit complete, on ne vous demande pas de
                                    reproduire de telles tautologies dans le devoir)
i := 1;

{n > 0 & i = 1}
{n > 0 & i = 1 & 0 = 0}

k := 0;

{n > 0 & i = 1 & k = 0}
{n > 0 & i = 1 & k = 0 & i = 2^k}        (l'invariant est vrai dans les conditions initiales)
while 2*i <= n do
begin
    i := 2*i;
    k := k+1;
end;
{i = 2^k & 2*i > n}
{2^(k+1) > n & k est le plus petit entier verifiant cette inegalite}
{2^(k+1) > n & 2^k <= n}
{2^k =< n < 2^(k+1)}

Ce qui acheve la preuve. Nous avons donc montre qu'avec la pre-condition n>0 (necessaire pour que la boucle se termine), le programme decrit permet de determiner l'entier k tel que 2^k =< n < 2^(k+1). k est donc la partie entiere de log2( n ).

II. Exercice 2

Il s'agit de calculer la somme double des entiers de 1 a N. L'idee pour trouver l'invariant est ici de regarder la conclusion.

Pour appliquer (1), il nous faut trouver un invariant P tel que {P & non B} implique {X = N * (N+1) * (N+2) / 6 }.

Or B correspond a J <> N. D'ou on cherche P tel que :
{P & J = N} => {X = N * (N+1) * (N+2) / 6 }

On pense alors evidemment a l'invariant X = J * (J+1) * (J+2) / 6.
Il est trivialement verifie pour J = X = 0 et nous permet de deduire la conclusion. Essayons maintenant de demontrer son invariance dans la boucle :

{ X = J * (J+1) * (J+2) / 6 & J <> N }

J := J+1;

{ X = (J-1) * J * (J+1) / 6 } (la condition J <> N ne nous interesse pas)

Y := Y + J;

On se rend compte ici du probleme de ne pas avoir inclu Y dans l'invariant, une instruction laisse nos conditions inchangees et nous ne pourrons pas deduire l'instruction suivante impliquant X et Y.

Il faut donc recommencer avec un invariant plus complet.
J est un compteur et a chaque tour de boucle, il est ajoute a Y. Y est donc la somme des entiers de 1 a N, c'est-a-dire J * (J+1) / 2.

L'invariant est donc a present :
{ X = J * (J+1) * (J+2) / 6 & Y = J * (J+1) / 2 }
L'invariant est bien vrai pour les conditions initiales et il nous permet bien sur d'obtenir la conclusion puisque c'etait deja le cas avec un invariant plus restreint.

{ X = J * (J+1) * (J+2) / 6 & Y = J * (J+1) / 2 & J <> N }

J := J+1;

{ X = (J-1) * J * (J+1) / 6 & Y = (J-1) * J / 2}

Y := Y + J;

On realise le calcul separement :

Y = (J-1) * J / 2 + J = J * ( (J-1) / 2 + 1) = J * (J+1) / 2

D'ou la post-condition :
{ X = (J-1) * J * (J+1) / 6 & Y = (J+1) * J / 2}

X := X + Y;

X = (J-1) * J * (J+1) / 6 + (J+1) * J / 2 = (J+1) * J / 2 * ( (J-1)/3 +1) = J * (J+1) * (J+2) / 6.

D'ou la post-condition :
{ X = J * (J+1) * (J+2) / 6 & Y = J * (J+1) / 2 }

On retrouve bien l'invariant.
D'autre part, il est evident que la boucle se termine puisque N - J prend la valeur 0 apres N tours de boucle. D'ou on peut appliquer (1) :

{ X = J * (J+1) * (J+2) / 6 & Y = J * (J+1) / 2 }
while J <> N do
begin
    J := J + 1;
    Y := Y + J;
    X := X + Y;
end;
{ X = J * (J+1) * (J+2) / 6 & Y = J * (J+1) / 2  & J = N}
Ce qui implique bien {X = N * (N+1) * (N+2) / 6}.

Pour finir rigoureusement la preuve, il suffit d'inclure cette preuve dans le programme globale avec les conditions initiales, comme dans la preuve de l'exercice 1.
 

Pour toutes questions ou remarques, n'hesitez pas : rigouste@site.uottawa.ca .