Consistance et complétude vis-à-vis de la sémantique opérationnelle

C'est ici qu'apparaît la notion de plus faible précondition.

Preuve de correction de l'algorithme d'Euclide pour le PGCD