Correction d'un algorithme

Un algorithme est correct s'il fait ce qu'on attend de lui. Plus précisément, rappelons qu'un algorithme est décrit par une spécification des données sur lesquelles l'algorithme va démarrer son calcul et une spécification du résultat produit par l'algorithme. Démontrer la correction de l'algorithme consiste à démontrer que l'algorithme retourne, quand il calcule en partant des données, un objet qui est un des résultats escomptés et qui satisfait la spécification du résultat comme énoncé dans la description de l'algorithme.

Correction partielle et terminaison

Pour s'assurer qu'un algorithme est correct, il faut démontrer deux choses: il faut démontrer que l'algorithme se termine (terminaison), autrement dit qu'il ne boucle pas ou ne diverge pas, produisant au moins un résultat et que le résultat de l'algorithme est effectivement de la forme énoncée par la spécification (correction partielle). La conjonction de la correction partielle et de la terminaison s'appelle la correction totale.

Correction d'un algorithme itératif

Comme la construction essentielle d'un algorithme itératif est la boucle (construction tant que ou while), l'argument principal de la démonstration de la correction partielle d'un algorithme itératif est la recherche d'un invariant pour chaque boucle (un invariant de boucle). Un invariant est un prédicat portant sur les variables du programme et sur des variables auxiliaires (ajoutées pour exprimer ce prédicat). La recherche des invariants est une opération difficile qui peut faire sortir de la logique utilisée pour décrire l'algorithme (incomplétude). Une fois ces invariants exhibés, le cœur de la démonstration consiste à démontrer que chaque invariant est effectivement stable lors de l'exécution de la boucle ; cela signifie que si l'invariant est satisfait avant l'exécution du corps de la boucle, il est satisfait après.

Correction d'un algorithme récursif

Pour démontrer la correction d'un algorithme récursif, il faut connaître une précondition (un prédicat satisfait avant l'appel de l'algorithme) et une postcondition (un prédicat satisfait après l'appel de l'algorithme). Il faut ensuite démontrer que l'algorithme satisfait ce couple (précondition, postcondition) en admettant qu'au cœur de l'algorithme les appels (récursifs) internes à l'algorithme satisfont ces couples (précondition, postcondition).