Correction des programmes

Un des problèmes le plus difficiles en programmation est celui de montrer la correction des programmes. On dit qu'un programme est correct, si:

• il termine pour n'importe quelle valeur de ses entrées (Terminaison),
• il fait ce que nous attendons de lui (Adéquation à la spécification).

Prenons toujours l'exemple du programme qui calcule, pour n'importe quel entier positif n, la somme 1 + 2 + ...+ n, et qui garde ce résultat dans la variable somme. Ce programme contient une boucle qui réalise incrémentalement le calcul. On dira qu'elle est correcte si:

• pour n'importe quelle valeur entière et positive de n, la boucle termine,

• en sortie de boucle, le résultat calculé dans somme est bien 1 + 2 + ...+ n.

La correction est une propriété mathématique des programmes. Montrer qu'un programme est correcte est une tâche ardue et en dehors de la portée de ce cours. Cependant, un minimum de conviction quant à la correction de son programme est nécessaire au programmeur qui veut avancer d'un bon pas dans son travail. Ainsi, dans cette partie nous n'avons comme ambition que celle de sensibiliser le lecteur au problème de la correction et de lui fournir quelques pistes pour se poser les bonnes questions à ce sujet ...et parfois, pour tenter d'y répondre.