L'essentiel: preuve d'algorithme par invariant de boucle

Plus de vidéos sur http://jjfpcsi1.github.io/CPGE-Kleber... 00:00 L'essentiel: preuve d'algorithme par invariant de boucle sur l'exemple de la factorielle. 4 étapes à respecter: 01:13 L'initialisation il s'agit de vérifier que la propriété invariante de boucle est vraie avant d'entrer dans la boucle 01:40 L'hérédité on vérifie que la propriété est bien conservée quand on passe du rang i au rang i+1 02:39 La terminaison on vérifie que la boucle se finit bien un jour ou l'autre 03:02 La correction en utilisant la propriété invariante de boucle connaissant la valeur d'une variable lors de la terminaison, on prouve que l'algorithme est correct, c'est-à-dire que la variable renvoyée à la fin contient bien la valeur attendu