Introduction informatique notion d’invariant de boucle

Cours introduction informatique notion d’invariant de boucle, tutoriel & guide de travaux pratiques en pdf.

Programmation impérative

1. Correction et terminaison

Etant donne un algorithme, il est important de verifier sa correction (ou sa validite), i.e. qu’il renvoie bien le resultat souhait´e, et sa terminaison, i.e. qu’il ne boucle pas ind´efiniment (pour certains algorithmes recursifs ou pour des boucles conditionnelles). Remarque : on peut egalement se poser la question de son efficacite (i.e. de sa rapidit´e et de l’espace qu’il prend), ce que nous ferons lors du cours sur la complexite. En r´ealit´e, on ne peut pas prouver, en toute generalite, la terminaison d’un algorithme donne. Penser `a la suite de Syracuse. Pire, on peut prouver qu’on ne peut pas le prouver. Nous ne rentrerons pas dans les d´etails de la preuve d’un programme imperatif : c’est un sujet delicat, qui peut vite devenir tres complique. Donnons le principe general de preuve d’une boucle.

2. Notion d’invariant de boucle

Une boucle, qu’elle soit conditionnelle ou inconditionnelle (on dit aussi indexee), peut se schematiser de la maniere suivante : On part d’une pr´econdition (ou condition d’entree) dans le module, qui d´ecrit l’etat des variables avant d’entrer dans la boucle. On effectue un certain nombre de passages dans la boucle, non n´ecessairement connu a l’avance. En sortie de boucle, la condition de sortie (ou postcondition), qui doit correspondre au resultat souhait´e. On appelle invariant de boucle un predicat sur les arguments de la boucle, renvoyant vrai avant passage dans la boucle, restant vrai apres passage dans la boucle : en sortie de boucle, l’invariant de boucle est vrai, ce qui doit nous permettre de prouver qu’on a obtenu le resultat souhaite. Remarque : il s’agit donc de montrer un resultat par recurrence finie. Prenons l’exemple de la fonction factorielle, de maniere imperative avec boucle indexee :
# let fact n = let temp = ref 1 in for i = 1 to n do temp := !temp ∗ i done; !temp ; ; fact : int −> int = <fun> # fact 5;; − : int = 120 Pourquoi cette fonction renvoie-t-elle bien la bonne valeur? La pr´econdition est : temp a pour valeur 1 . Montrons que pour tout k ∈ [[0,n]], la valeur de temp apr`es la k-`eme it´eration est k!. C’est vrai pour k = 0 (avant l’entr´ee dans la boucle), et, supposant la propri´et´e vraie `a un rang k ∈ [[0,n−1]], alors apr`es un nouveau passage dans la boucle (pour i = k + 1), la valeur de temp est (k + 1)!. En sortie de boucle, i.e. apr`es la n-i`eme it´eration, on obtient n! comme valeur pour temp. En fait, il n’est pas n´ecessaire de tant d´etailler la correction de cette boucle (une preuve n’est pas syst´ematique). On se contentera de mettre en commentaire l’invariant de boucle :
# let fact n = let temp = ref 1 in for i = 1 to n do temp := !temp ∗ i done; (∗ invariant : ! temp = i ! ∗) !temp ; ; fact : int −> int = <fun>