"Démontrer" qu'un programme a l'effet souhaité

Exemple: échanger deux variables

Exemple: échange conditionnelle

Les boucles

Démontrer qu'une condition est vraie après une boucle

Prendre l'exemple d'une boucle
  tant que ExpressionBooleenne faire
     BlocInstruction
  fintantque;

Trouver une assertion ``invariante'' telle que

Un exemple très simple

la somme des éléments d'un tableau T[1..n]:

i:=1;
s:=0;
tant que i<=n faire
   s:=s+T[i];
   i:=i+1
fintantque;

Terminaison des boucles

Un (mauvais) algorithme de tri

Autres exemples

Des cas ou le bon invariant aide à concevoir l'algorithme?

Un invariant peut servir à:
concevoir
expliquer
documenter
comprendre
tester
un algorithme

Trouver le vainqueur d'une élection

Les procédures et fonctions




File translated from TEX by TTH, version 3.05.
On 27 Nov 2006, 12:21.