"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 16 Nov 2005, 10:08.

symboles bricolés par sed