Voir la source de Algorithmique/Preuve d'arrêt

{{Chapitre
  | niveau    = 14
  | idfaculté = informatique
  | numéro    = 3
  | précédent = [[../Variables/]]
  | suivant   = [[../Forme d'écriture|Forme d'écriture d'un algorithme]]
}}

Comme nous le savons, un algorithme est une séquence d'instructions créée dans l'optique de résoudre un problème. Il est alors important de vérifier que notre séquence réalise bien ce qu'on lui demande.

Avant cela, il est primordial d'étudier ce qu'on nomme ''la preuve d'arrêt'' d'un algorithme. C'est ce que nous ferons dans cette présente leçon.

== Quelques exemples  ==
Imaginons un algorithme tel que :

{{Exemple
  | contenu =
<syntaxhighlight lang="text">
Début
----
i ← 1
Tant que i < 10 faire
    Afficher i
Fin Tant que
----
Fin
</syntaxhighlight>
}}

Ici, le problème est simple : on réalise une condition qui sera toujours vérifiée car la variable reste identique. L'algorithme tournera alors à l'infini.

Voyons un autre exemple :

{{Exemple
  | contenu =
<syntaxhighlight lang="text">
Début
----
i ← 100
Tant que i > 0 faire
    Afficher i
    i ← i - 1
Fin Tant que
----
Fin
</syntaxhighlight>
}}

Là, l'algorithme s'arrête. Voyons comment noter la preuve de cet arrêt.

== Écriture formelle de la preuve d'arrêt  ==
Reprenons l'algorithme précédent. Nous avons une boucle qui réalise une comparaison itérative. À l'intérieur de cette boucle est opéré un certain nombre d'instructions mais l'élément primordial est la réaffectation de i. Sans celle-ci, nous aurions le même problème que pour le premier algorithme.

Formellement, notre algorithme s'arrête car i<math>_0</math> est positif ET qu’il décroit strictement. L'arrêt est donc réalisé car la comparaison i > 0 sera fausse à un certain moment.

{{Bas de page
  | idfaculté = informatique
  | précédent = [[../Variables/]] 
  | suivant   = [[../Forme d'écriture|Forme d'écriture d'un algorithme]]
}}