INGIniousLa plus forte postcondition (\(sp\))
Chercher l'assertion \(Q\) la plus forte dans un triplet de Hoare \(\{P\}\ S\ \{Q\}\), c'est appliquer la méthode progressive. On calcule la plus forte postcondition \(sp(S, P)\) en partant de la précondition \(P\) et en évaluant les instructions de \(S\) une par une, ce qui donne la postcondition la plus restrictive garantie après l'exécution de \(S\) quand on part d'un état qui vérifie \(P\).
Une assertion plus restrictive est correcte si elle reste vraie pour toutes les exécutions possibles et la plus forte si elle n'exclut aucune valeur pourtant atteignable.
Les règles de calcul
| Type d'instruction | Règle formelle | Intuition |
|---|---|---|
| Affectation (\(x = e\)) | \(sp(x = e, P) = P[x/x'] \land x = e[x/x']\) | Après l'affectation, on renomme l'ancienne valeur de \(x\) en \(x'\) dans la précondition et on ajoute que la nouvelle valeur de \(x\) vaut l'expression \(e\). |
| Séquence (\(S_1; \dots; S_n\)) | \(sp(S_1; \dots; S_n, P) = A_n\) où \(A_0 = P\) et \(A_i = sp(S_i, A_{i-1})\) | On calcule la plus forte postcondition de chaque instruction, dans l'ordre où elles apparaissent. |
| Condition (\(\texttt{if (B) \{S1\} else \{S2\}}\)) | \(sp(\texttt{if (B) \{S1\} else \{S2\}}, P) = sp(S1, P \land B) \lor sp(S2, P \land \neg B)\) | On suit les deux branches : la \(sp\) de la branche then avec \(B\) vraie, disjonctée avec celle de la branche else avec \(B\) fausse. |
| Assignation tabulaire (\(a[s] = e\)) | \(sp(a[s] = e, P) = P[a/a'] \land a[s[a/a']] = e[a/a'] \land \forall i \neq s[a/a'] : a[i] = a'[i]\) | Même principe que l'affectation simple mais adapté aux tableaux : seule la case d'indice \(s\) change, les autres cases restent inchangées. |
| Boucle (\(\texttt{while (B) \{S\}}\)) | \(sp(\texttt{while (B) \{S\}}, P) = I \land \neg B\) où \(I\) est un invariant de la boucle tel que \(P \Rightarrow I\) | Le nombre d'itérations est inconnu, mais un invariant vrai avant la boucle reste vrai après chaque itération. A la sortie, il est donc encore vérifié, accompagné de la condition d'arrêt \(\neg B\). |