Introduction
Lorsque l'on écrit un programme informatique, il est souvent bienvenu de prouver que ce programme fait bien ce qu'il promet de faire.
En effet, si l'on prend l'exemple de la conduite autonome, il est bon de savoir que notre voiture va bien freiner lorsqu'elle repère un obstacle.
On va donc ici s'intéresser à la correction des algorithmes et des boucles.