« Algorithmique/Preuve d'arrêt » : différence entre les versions

Une page de Wikiversité, la communauté pédagogique libre.
Contenu supprimé Contenu ajouté
→‎Quelques exemples : maintenance - wikification
RM77 (discussion | contributions)
Ligne 37 : Ligne 37 :
<source lang="text">
<source lang="text">
Début
Début
i = 100<
i = 100
Tant que i > 0
Tant que i > 0
Afficher i
Afficher i

Version du 4 août 2011 à 23:44

Début de la boite de navigation du chapitre
Preuve d'arrêt
Icône de la faculté
Chapitre no {{{numéro}}}
Leçon : Algorithmique
Chap. préc. :Variables
Chap. suiv. :Forme d'écriture d'un algorithme
fin de la boite de navigation du chapitre
En raison de limitations techniques, la typographie souhaitable du titre, « Algorithmique : Preuve d'arrêt
Algorithmique/Preuve d'arrêt
 », n'a pu être restituée correctement ci-dessus.

Comme nous le savons, un algorithme est une séquence d'instructions dans le but 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

Rien de mieux qu'un exemple pour comprendre ce qu'est la preuve d'arrêt.

Imaginons un algorithme tel que :

Début de l'exemple
Fin de l'exemple


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 :

Début de l'exemple
Fin de l'exemple


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'instruction 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 est positif ET que i décroit strictement. L'arrêt est donc réalisé car la comparaison i > 0 sera fausse à un certain moment.