Que represente {P} C {Q} en logique de Hoare ?

Un commentaire Un triplet : si P avant C, Q apres (si C termine) Une assertion de compilation Un type Valider