Département d'Informatique
Maîtrise d'Informatique 2001/2002
Spécifications formelles, preuves
& construction de programmes
Travaux dirigés
Mercredi 21 novembre










Logique de Hoare






Où l'on utilise le triplet de Hoare {p}P{q} et les règles de déduction associées, pour faire la preuve de correction de programmes impératifs.






1   Quelques extraits de programmes

Démontrer les théorèmes suivants (indiquer les règles à utiliser) :
  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}

2   Itération et invariant

On désire démontrer le théorème suivant :



{x=0 /\ y=a}
while y<>0 do {
x:=x+b;
y:=y-1
}
{x=a × b}




  1. Montrer que x + (y × b) = a × b est un invariant de l'itération ci-dessus.

  2. En déduire la preuve de ce théorème.

3   Recherche d'invariant

Trouver un invariant (en décomposant la post-condition), puis démontrer les théorèmes suivants :


  1. Somme de deux entiers 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 n  :
    {vrai} 
    c:=0;i:=0;
while i<>n do {
  c:=c+2*i+1;
  i:=i+1
}
    {c=n2}

4   Correction totale

Le programme suivant calcule la somme des diviseurs d'un entier n . Démontrer la correction partielle (écrire la post-condition et trouver un invariant), puis montrer la terminaison.


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



Mêmes questions pour le programme suivant qui calcule le n-ième terme de la suite de Fibonacci.


  f:=1;i:=1;u:=0;
  while i<>n do {
    z:=f;f:=f+u;u:=z;
    i:=i+1
  }
This document was translated from LATEX by HEVEA.