Programmes justes : logique de Hoare et invariants

Cours · algorithmique (école d'ingénieur), chapitre 11 · école d'ingénieur, informatique · le début du chapitre, la suite sur Adloun

Objectifs du chapitre

Donner un sens précis aux instructions d'un programme à l'aide des triplets de Hoare.
Écrire une boucle à partir d'une propriété invariante : initialisation, progression, arrêt, terminaison.
Commenter un programme par ses invariants.
Appliquer la méthode à des problèmes classiques résolus en $Θ (n)$ ou en $Θ (lo g n)$ .

Un programme qui « marche sur les exemples » n'est pas pour autant un programme juste. Les tests montrent la présence d'erreurs, jamais leur absence. Ce chapitre présente une façon de construire des programmes justes : on part de ce que le programme doit établir, on choisit une propriété qui reste vraie tout au long du calcul, et l'on écrit les instructions qui la préservent. Les commentaires des programmes ne décrivent alors plus ce que fait une instruction, mais ce qui est vrai après son exécution.

11.1 Assertions et triplets de Hoare

Définition 11.1Assertion

Une assertion est une propriété des variables d'un programme, qui est vraie ou fausse en un point donné de son exécution. Par exemple « $s = \sum_{i \in [0 : k]} T [i]$ » ou « $x \leq y$ ».

Définition 11.2Triplet de Hoare

Soient $P$ et $Q$ deux assertions et $S$ une instruction. Le triplet de Hoare ${P} S {Q}$ signifie : si $P$ est vraie avant l'exécution de $S$ , et si $S$ se termine, alors $Q$ est vraie après. $P$ est la précondition, $Q$ la postcondition.

Exemple 11.3quelques triplets

${x = 3}$ x = x + 1; ${x = 4}$ est vrai.
${x \geq 0}$ x = x + 1; ${x > 0}$ est vrai.
${vrai}$ if (x < 0) x = -x; ${x \geq 0}$ est vrai (aux dépassements de capacité près).
${x > 0}$ x = x - 1; ${x > 0}$ est faux : prendre $x = 1$ .

C. A. R. Hoare (né en 1934, également inventeur du tri rapide) a proposé en 1969 des règles qui donnent la signification de chaque construction d'un langage de programmation. Les voici, pour le petit noyau de Java que nous utilisons.

11.1.1 L'affectation

Proposition 11.4Règle de l'affectation

Pour toute assertion $Q$ :

${Q [x \leftarrow E]}$ x = E; ${Q}$

où $Q [x \leftarrow E]$ est l'assertion $Q$ dans laquelle chaque occurrence de $x$ est remplacée par l'expression $E$ .

La règle se lit à rebours : pour que $Q$ soit vraie après x = E;, il faut et il suffit que $Q$ , où l'on remplace $x$ par $E$ , soit vraie avant.

Exemple 11.5calculer une précondition

Quelle précondition garantit $s = \sum_{i \in [0 : k + 1]} T [i]$ après s = s + T[k]; ? On remplace $s$ par $s + T [k]$ :

$s + T [k] = i \in [0 : k + 1] \sum T [i] ⟺ s = i \in [0 : k] \sum T [i] .$

C'est exactement « $s$ est la somme du $k$ -préfixe ».

11.1.2 La séquence et la conséquence

Proposition 11.6Règles de la séquence et de la conséquence

Séquence. Si ${P} S_{1} {R}$ et ${R} S_{2} {Q}$ , alors ${P} S_{1} S_{2} {Q}$ .

Conséquence. Si $P \Rightarrow P^{'}$ , ${P^{'}} S {Q^{'}}$ et $Q^{'} \Rightarrow Q$ , alors ${P} S {Q}$ .

Exemple 11.7échanger deux variables

Montrons ${x = a \land y = b}$ t = x; x = y; y = t; ${x = b \land y = a}$ . On remonte depuis la postcondition, en appliquant la règle de l'affectation à chaque instruction, de la dernière à la première :

${x = b \land t = a}$ y = t; ${x = b \land y = a}$ ;
${y = b \land t = a}$ x = y; ${x = b \land t = a}$ ;
${y = b \land x = a}$ t = x; ${y = b \land t = a}$ .

La précondition obtenue est exactement $x = a \land y = b$ . La règle de la séquence permet de conclure.

11.1.3 La conditionnelle

Proposition 11.8Règle de la conditionnelle

Si ${P \land B} S_{1} {Q}$ et ${P \land \neg B} S_{2} {Q}$ , alors

${P}$ if (B) S1 else S2 ${Q}$ .

Autrement dit, il faut vérifier chaque branche, en sachant dans laquelle on se trouve. C'est le raisonnement par cas que nous avons fait sans le dire dans toutes les équations de récurrence de la première partie.

11.1.4 La boucle

Proposition 11.9Règle de la boucle

Si ${I \land B} S {I}$ , alors

${I}$ while (B) S ${I \land \neg B}$ .

L'assertion $I$ est un invariant de la boucle.

Cette règle est le cœur de la méthode. Si $I$ est vraie avant la boucle, et si chaque tour préserve $I$ , alors à la sortie de la boucle on sait deux choses : $I$ est vraie, et la condition $B$ est fausse. Le choix de $I$ est fait pour que ces deux faits réunis donnent le résultat attendu.

La suite du cours est sur Adloun

Le chapitre en entier, formules et figures comprises, avec le tuteur, les fiches, les QCM et les exercices.

Lire la suite du cours

En accès libre, sans inscription.

Exercices corrigés de ce chapitre

Lire la suite du cours →