Correction de la logique de Hoare

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.