On prouve ici la correction de la logique de Hoare. On insistera sur le cas de la boucle while que est le cas le plus intéressant.