Plus faible précondition — exercice corrigé d'algorithmique (école d'ingénieur) (chapitre 11)

Plus faible précondition

Programmes justes : logique de Hoare et invariants · niveau 2

Énoncé

Calculer la plus faible précondition $P$ qui rend vrai chacun des triplets suivants (les variables sont entières).

${P}$ y = x * x; x = y + 1; ${x > 10}$
${P}$ if (x < 0) x = -x; x = x - 1; ${x \geq 0}$
${P}$ s = s + T[k]; k = k + 1; ${s = \sum_{i \in [0 : k]} T [i]}$ . Que retrouve-t-on ?

Avant x = y + 1; : $y + 1 > 10$ , soit $y > 9$ . Avant y = x * x; : $x^{2} > 9$ . Donc $P \equiv ∣ x ∣ > 3$ , c'est-à-dire $x \leq - 4$ ou $x \geq 4$ .
Avant x = x - 1; : $x \geq 1$ . Pour la conditionnelle (sans else) : $P \equiv (x < 0 \Rightarrow - x \geq 1) \land (x \geq 0 \Rightarrow x \geq 1)$ , soit $(x \leq - 1) \lor (x \geq 1)$ , c'est-à-dire $x \neq = 0$ .
Avant k = k + 1; : $s = \sum_{i \in [0 : k + 1]} T [i]$ . Avant s = s + T[k]; : $s + T [k] = \sum_{i \in [0 : k + 1]} T [i]$ , c'est-à-dire $s = \sum_{i \in [0 : k]} T [i]$ . On retrouve l'invariant de la somme d'un tableau : le corps de boucle le conserve.