Triplets de Hoare — exercice corrigé d'algorithmique (école d'ingénieur) (chapitre 11)

Triplets de Hoare

Programmes justes : logique de Hoare et invariants · niveau 1 (application)

Énoncé

Dire si les triplets suivants sont vrais. Pour ceux qui sont faux, donner un contre-exemple ; pour ceux qui sont vrais, calculer la plus faible précondition avec la règle de l'affectation.

${x > 2}$ x = 2 * x - 1; ${x > 3}$
${x = a \land y = b}$ x = x + y; y = x - y; x = x - y; ${x = b \land y = a}$
${vrai}$ if (x > y) m = x; else m = y; ${m = max (x, y)}$
${x \geq 0}$ x = x / 2; ${2 x = ancienne valeur de x}$

Corrigé

Vrai. La règle de l'affectation donne la plus faible précondition $2 x - 1 > 3$ , c'est-à-dire $x > 2$ : c'est exactement $P$ .
Vrai. On remonte les trois affectations depuis la postcondition :

$avant x = x - y : avant y = x - y : avant x = x + y : x - y = b \land y = a x - (x - y) = b \land x - y = a, soit y = b \land x - y = a y = b \land (x + y) - y = a, soit x = a \land y = b .$

La plus faible précondition est la précondition donnée. (En Java, le dépassement de capacité ne casse pas l'échange : les calculs sont exacts modulo $2^{32}$ .)

Vrai. Règle de la conditionnelle : il faut ${x > y} m = x {m = max (x, y)}$ , vrai car alors $max (x, y) = x$ , et ${x \leq y} m = y {m = max (x, y)}$ , vrai de même. La plus faible précondition est $vrai$ .
Faux : pour $x = 3$ , après x = x / 2; on a $x = 1$ et $2 x = 2 \neq = 3$ . La division entière perd le bit de poids faible ; le triplet n'est vrai que pour $x$ pair.