INGIniousLa plus faible précondition (\(wp\))
Chercher l'assertion \(P\) la plus faible dans un triplet de Hoare \(\{P\}\ S\ \{Q\}\), c'est appliquer la méthode régressive. On calcule la plus faible précondition \(wp(S, Q)\) en partant de la postcondition \(Q\) et en remontant les instructions de \(S\) une par une, ce qui donne la précondition la plus générale qui garantit \(Q\) après l'exécution de \(S\).
Les règles de calcul
| Type d'instruction | Règle formelle | Intuition |
|---|---|---|
| Affectation (\(x = e\)) | \(wp(x = e, Q) = Q[x/e]\) | Il suffit d'avoir une version de \(Q\) où les occurrences de \(x\) sont remplacées par \(e\) pour garantir \(Q\) après l'affectation. |
| Séquence (\(S_1; \dots; S_n\)) | \(wp(S_1; \dots; S_n, Q) = A_0\) où \(A_n = Q\) et \(A_i = wp(S_i, A_{i+1})\) | On raisonne à l'envers : on part de la postcondition et on remonte la séquence dans l'ordre inverse de leur exécution. |
| Condition (\(\texttt{if (B) \{S1\} else \{S2\}}\)) | \(wp(\texttt{if (B) \{S1\} else \{S2\}}, Q) = (B \Rightarrow wp(S1, Q)) \land (\neg B \Rightarrow wp(S2, Q))\) | Chaque branche doit garantir \(Q\) sous sa condition respective. |
| Assignation tabulaire (\(a[s] = e\)) | \(wp(a[s] = e, Q) = Q\langle a[s] \leftarrow e \rangle\) | On applique une substitution à l'expression \(a[s]\) plutôt qu'un simple remplacement textuel (voir ci-dessous) car remplacer du texte pourrait toucher une autre case du même tableau, comme \(a[5]\) quand on affecte \(a[k]\) avec \(k \neq 5\). |
| Boucle (\(\texttt{while (B) \{S\}}\)) | \(wp(\texttt{while (B) \{S\}}, Q) = I\) où \(I\) est un invariant de la boucle tel que \(I \land \neg B \Rightarrow Q\) | Raisonner à l'envers revient à chercher l'invariant qui, combiné à la condition d'arrêt \(\neg B\), implique \(Q\). Cet invariant est alors exactement ce qui doit être vrai avant la boucle. |
L'application d'une substitution
Soit \(s\) une expression et \(u \leftarrow t\) une substitution. L'application de la substitution à l'expression, notée \(s\langle u \leftarrow t \rangle\), est définie comme suit :
- si \(s\) est une variable simple, alors \(s\langle u \leftarrow t \rangle = \left\{ \begin{array}{ll} t & \mbox{si } s \equiv u \\ s & \mbox{sinon} \end{array} \right.\)
- si \(s\) est une constante, alors \(s\langle u \leftarrow t \rangle = s\)
- si \(s = op(s_1, s_2)\) pour un opérateur \(op\), alors \(s\langle u \leftarrow t \rangle = op(s_1\langle u \leftarrow t \rangle, s_2\langle u \leftarrow t \rangle)\)
- si \(s\) est une variable indicée \(a[e]\) et si \(u\) est une variable simple ou \(u\) de la forme \(b[e']\) avec \(a \neq b\), alors \(s\langle u \leftarrow t \rangle = a[e\langle u \leftarrow t \rangle]\)
- si \(s\) est une variable indicée \(a[e]\) et si \(u\) est de la forme \(a[e']\), alors \(s\langle u \leftarrow t \rangle = \left\{ \begin{array}{ll} t & \mbox{si } e\langle u \leftarrow t \rangle = e' \\ a[e\langle u \leftarrow t \rangle] & \mbox{sinon} \end{array} \right.\)
- si \(s = \mbox{si } B \mbox{ alors } s_1 \mbox{ sinon } s_2\), alors \(s\langle u \leftarrow t \rangle = \mbox{si } B\langle u \leftarrow t \rangle \mbox{ alors } s_1\langle u \leftarrow t \rangle \mbox{ sinon } s_2\langle u \leftarrow t \rangle\)
Exemple
\(wp(\texttt{a[k] = 0;},\ a[5] = 0) \equiv (si\ k = 5\ alors\ 0\ sinon\ a[5]) = 0\)