Variables et boucles : la logique de Hoare