Exercices sur la logique d'Hoare

Quelques extraits de programmes à justifier

1. {x≥ 0} y:=x+1 {y>0}
2. {vrai} a:=x;b:=x {a=b}
3. {a>0} if a>b then b:=a {b>0}

Itération et invariant

    {x=0 et y=a}
    while y<>0 do {
        x := x+b;
        y := y-1;
    }
    {x = a*b}

1. On travaille avec des entiers naturels.
   1. Montrez que x + y*b = a*b un invariant de la boucle ci-dessus.
   2. Donnez la preuve de correction
   3. A quelle condition cette boucle termine-t-elle ? Quelle est la fonction de rang qui justifie la terminaison ?
2. Mêmes questions si on travaille avec des entiers relatifs.

Recherche d'invariant

1. Somme de deux entiers naturels n et m  :

     
       {vrai}
       a:=n;
       b:=m;
       while b<>0 do {
           a:=a+1;
           b:=b-1
       }
       {a=n+m}
     

2. Carré d'un entier naturel n  :

       {vrai}
       c:=0;
       i:=0;
       while i<>n do {
           c:=c+2*i+1;
           i:=i+1
       }
       {c=n*n}
     

Correction totale

1. Le programme ci-dessous calcule la somme des diviseurs d'un entier naturel n . Démontrez la correction partielle (pré-condition, post-condition, invariant et preuve), puis montrez la terminaison.

     
       d:=1;
       s:=0;
       while d<>n do {
           if n mod d = 0 then s:=s+d;
           d:=d+1
       }
   

2. Mêmes questions pour le programme suivant qui calcule le n-ième terme de la suite de Fibonacci définie par fib(0)=0, fib(1)=1 et fib(n+2)=fib(n+1)+fib(n) pour tout entier naturel n.

     
       f:=1;
       i:=1;
       u:=0;
       while i<>n do {
           z:=f;
           f:=f+u;
           u:=z;
           i:=i+1
       }