Correction d'un algorithme
From Wikipedia, the free encyclopedia
Cet article est une ébauche concernant la logique, l’informatique et l’informatique théorique.
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.
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)[1]. La conjonction de la correction partielle et de la terminaison s'appelle la correction totale.
