Logique de Hoare

Notations

Un triplet de Hoare est consitué d'une précondition $F$ et d'une postcondition $G$ qui sont toutes deux des formules du calcul des prédicats, et d'un programme prog. On note le triplet de deux façons différentes en fonction de la sémantique associée :

la notation $\newcommand{\cpartial}[1]{\left\{{#1}\right\}}\newcommand{\ctotal}[1]{\left\langle{#1}\right\rangle}\newcommand{\hptriple}[3]{\cpartial{#1}\ \mathtt{\text{#2}}\ \cpartial{#3}}\newcommand{\httriple}[3]{\ctotal{#1}\ \mathtt{\text{#2}}\ \ctotal{#3}}\hptriple{F}{prog}{G}$ désigne la correction partielle : le triplet est vrai (partiellement correct) si pour tout valuation qui rend $F$ vraie et telle que prog s'arrête, alors, après l'exécution et l'arrêt de prog, $G$ est vraie.
la notation $\httriple{F}{prog}{G}$ désigne la correction totale : le triplet est vrai (totalement correct) si pour tout valuation qui rend $F$ vraie, prog s'arrête et, après son exécution, $G$ est vraie.

Axiomes

La logique de Hoare est basée sur deux axiomes portant sur l'affectation. Dans ces axiomes, la notation $F[x\leftarrow T]$ désigne la formule $F$ du calcul des prédicats dans laquelle toutes les occurrence de la variable libre $x$ ont été remplacées par le terme $T$. La même notation est utilisée pour remplacer les occurrences d'une variable dans un terme par un autre terme.

Axiomes de Hoare

Les axiomes de Hoare pour l'affectation sont de la forme :

$\newcommand{\egal}{\,\leftarrow\,} \begin{array}{c} \phantom{\httriple{F[x\leftarrow T]}{x $\egal$ T}{F}} \\\hline \httriple{F[x\leftarrow T]}{x $\egal$ T}{F} \end{array}\leftarrow \text{ Hoare} $

Axiomes de Floyd

Les axiomes de Floyd pour l'affectation sont de la forme :

$ \begin{array}{c} \phantom{\httriple{F[x\leftarrow T]}{x $\egal$ T}{F}} \\\hline \httriple{F}{x $\egal$ T}{(\exists y, (F[x\leftarrow y]\land (x=T[x\leftarrow y])))} \end{array}\leftarrow \text{ Floyd} $

Règles de déduction

Le reste du système consiste en les règles de déduction suivantes.

Règles simples

$ \begin{array}{c} \httriple{F}{prog1}{G}\phantom{\text{prog}}\httriple{G}{prog2}{H} \\\hline \httriple{F}{prog1; prog2}{H} \end{array}\text{ ;} $

$\newcommand{\limplies}[0]{\Rightarrow} \begin{array}{c} (F\limplies G)\phantom{\text{prog}} \httriple{G}{prog}{H} \phantom{\text{prog}} (H\limplies I) \\\hline \httriple{F}{prog}{I} \end{array}\limplies $

$ \begin{array}{c} \httriple{(F\land b)}{prog1}{G} \phantom{\text{prog}} \httriple{(F\land (\lnot b))}{prog2}{G} \\\hline \httriple{F}{if ($b$) prog1 else prog2 end if}{G} \end{array}\text{ if then} $

Règles pour les boucles

Correction partielle

La correction partielle d'une boucle while consiste simplement à faire l'hypothèse que si la boucle possède un invariant, alors celui-ci sera vrai après l'arrêt de la boucle (s'il était vrai avant). Ceci correspond à la règle suivante :

$ \begin{array}{c} \hptriple{(I \land b)}{prog}{I} \\\hline \hptriple{I}{while($b$) prog end while}{(I\land(\lnot b))} \end{array}\text{ while partiel} $

dans laquelle $I$ est l'invariant.

Correction totale

Pour la correction totale, il faut aussi garantir l'arrêt de la boucle, ce qui peut se faire grâce à un variant. Il s'agit d'un terme $V$ dont la valeur décroît strictement à chaque exécution de la boucle, tout en restant de façon garantie supérieure ou égale à zéro. Comme les programmes travaillent en valeurs entières, ces propriétés garantissent l'arrêt de la boucle. On a donc la règle suivante :

$ \begin{array}{c} \httriple{(I \land b\land (V=n))}{prog}{I\land (V<n)\land (V\geq 0))} \\\hline \httriple{I}{while(\(b$) prog end while}{(I\land(\lnot b))} \end{array}\text{ while total} \)

dans laquelle $I$ est l'invariant, $V$ le variant et $n$ une variable qui n'apparaît ni dans $V$, ni dans $I$, ni dans prog.