Module HoareLogic

From Coq Require Import ZArith Psatz Bool String List Wellfounded Program.Equality.
From Coq Require Import FunctionalExtensionality.
From CDF Require Import IMP Sequences.

Local Open Scope string_scope.
Local Open Scope Z_scope.

4. Logiques de programmes: logique de Hoare


4.1. Prologue: vérifier directement un programme


On peut vérifier la correction d'un programme en utilisant uniquement la sémantique opérationnelle du langage dans lequel il est écrit. Par exemple, voici un programme IMP qui échange les valeurs de deux variables.

Definition swap_xy :=
  ASSIGN "t" (VAR "x");; ASSIGN "x" (VAR "y");; ASSIGN "y" (VAR "t").

On peut caractériser le comportement attendu du programme comme suit: démarré dans un état mémoire s, il termine toujours et dans un état mémoire s' où "x" vaut s "y" et "y" vaut s "x".

Lemma swap_xy_correct:
  forall s, exists s',
  star red (swap_xy, s) (SKIP, s') /\ s' "x" = s "y" /\ s' "y" = s "x".
Proof.
  intros. econstructor; split.
- eapply star_step. apply red_seq_step. apply red_assign.
  eapply star_step. apply red_seq_done.
  eapply star_step. apply red_seq_step. apply red_assign.
  eapply star_step. apply red_seq_done.
  eapply star_step. apply red_assign.
  apply star_refl.
- unfold update; cbn. auto.
Qed.

La démonstration est longue mais pas très difficile. Dans un premier temps on fait l'exécution "symbolique" du programme en enchaînant les étapes de réduction. Cela détermine l'état final s', qui vérifie facilement la propriété attendue.

Voici un exemple plus compliqué car il fait appel à une boucle. Le programme ajoute "x" à "y" en incrémentant "y" et décrémentant "x" jusqu'à ce que "x" tombe à zéro.

Definition slow_add :=
  WHILE (LESSEQUAL (CONST 1) (VAR "x"))
        (ASSIGN "x" (MINUS (VAR "x") (CONST 1)) ;;
         ASSIGN "y" (PLUS (VAR "y") (CONST 1))).

L'énoncé de correction du programme reste simple.

Lemma slow_add_correct:
  forall s,
  s "x" >= 0 ->
  exists s', star red (slow_add, s) (SKIP, s') /\ s' "y" = s "y" + s "x".
Proof.
  assert (REC: forall v, 0 <= v ->
               forall s, s "x" = v ->
               exists s', star red (slow_add, s) (SKIP, s') /\ s' "y" = s "y" + s "x").
  { intros v0 v0POS. pattern v0. apply natlike_ind; auto.
  - intros. exists s; split.
    + apply star_one. apply red_while_done. cbn. rewrite H. apply Z.leb_nle. lia.
    + lia.
  - intros v VPOS REC s EQ.
    set (s1 := update "x" v s).
    set (s2 := update "y" (s "y" + 1) s1).
    destruct (REC s2) as (s' & REDS & EQ'). auto.
    exists s'; split.
    + eapply star_step. apply red_while_loop. cbn. rewrite EQ. apply Z.leb_le. lia.
      eapply star_step. apply red_seq_step. apply red_seq_step. apply red_assign.
      eapply star_step. apply red_seq_step. apply red_seq_done.
      eapply star_step. apply red_seq_step. apply red_assign.
      eapply star_step. apply red_seq_done.
      cbn. replace (s "x" - 1) with v by lia. apply REDS.
    + rewrite EQ'. cbn. lia.
  }
  intros. eapply REC; eauto. lia.
Qed.

En revanche, la démonstration devient difficile. Il faut faire une récurrence explicite sur la valeur v de la variable "x". Pour exploiter l'hypothèse de récurrence, il faut déterminer manuellement certains états mémoire intermédiaires: l'exécution purement symbolique ne suffit plus. On ne se voit pas vérifier des programmes beaucoup plus complexes avec ces techniques.

Les logiques de programmes fournissent des principes de plus haut niveau pour vérifier formellement des programmes. En particulier, on peut raisonner sur les boucles sans faire de récurrence explicite.

La logique de programmes la plus connue est la logique de Hoare. Dans ce fichier, nous construisons une logique de Hoare pour raisonner sur les programmes écrits en langage IMP.

4.2. Assertions sur l'état mémoire


La logique de Hoare manipule des formules / des énoncés / des assertions qui "parlent" des valeurs des variables du programme. Une assertion typique est 0 <= x /\ x <= y, signifiant "à ce point du programme, la valeur de la variable x est positive et inférieure ou égale à la valeur de y".

Dans notre développement Coq, nous représentons les assertions par des formules logique de Coq (type Prop) paramétrées par un état mémoire (type store) qui donne des valeurs aux variables. Par exemple, l'assertion 0 <= x /\ x <= y ci-dessus est représentée par fun s => 0 <= s "x" /\ s "x" <= s "y".
    
Definition assertion : Type := store -> Prop.

Voici quelques assertions utiles. La conjonction et la disjonction de deux assertions.

Definition aand (P Q: assertion) : assertion :=
  fun s => P s /\ Q s.

Definition aor (P Q: assertion) : assertion :=
  fun s => P s \/ Q s.

L'assertion "l'expression arithmétique a s'évalue en la valeur v".

Definition aequal (a: aexp) (v: Z) : assertion :=
  fun s => aeval a s = v.

Les assertions "l'expression booléenne b s'évalue à vrai / à faux".

Definition atrue (b: bexp) : assertion :=
  fun s => beval b s = true.

Definition afalse (b: bexp) : assertion :=
  fun s => beval b s = false.

L'assertion notée " P[x <- a] " dans les articles. Substituer x par a dans P, cela revient à évaluer P dans des états mémoire où la variable x est égale à la valeur de l'expression a.

Definition aupdate (x: ident) (a: aexp) (P: assertion) : assertion :=
  fun s => P (update x (aeval a s) s).

L'implication point-à-point. Contrairement à la conjonction et la disjonction, ce n'est pas une assertion sur l'état mémoire, juste une proposition Coq.

Definition aimp (P Q: assertion) : Prop :=
  forall s, P s -> Q s.

Quelques notations pour faciliter la lecture.

Notation "P -->> Q" := (aimp P Q) (at level 95, no associativity).
Notation "P //\\ Q" := (aand P Q) (at level 80, right associativity).
Notation "P \\// Q" := (aor P Q) (at level 75, right associativity).

4.3. Règles de la logique de Hoare faible


Voici les règles de base de la logique de Hoare. Elles définissent une relation Hoare P c Q, avec Il s'agit d'une logique "faible" au sens où elle ne garantit pas la terminaison de c. La seule garantie est que si c termine, alors l'état final satisfait la postcondition Q.

Inductive Hoare: assertion -> com -> assertion -> Prop :=
  | Hoare_skip: forall P,
      Hoare P SKIP P
  | Hoare_assign: forall P x a,
      Hoare (aupdate x a P) (ASSIGN x a) P
  | Hoare_seq: forall P Q R c1 c2,
      Hoare P c1 Q ->
      Hoare Q c2 R ->
      Hoare P (c1;;c2) R
  | Hoare_ifthenelse: forall P Q b c1 c2,
      Hoare (atrue b //\\ P) c1 Q ->
      Hoare (afalse b //\\ P) c2 Q ->
      Hoare P (IFTHENELSE b c1 c2) Q
  | Hoare_while: forall P b c,
      Hoare (atrue b //\\ P) c P ->
      Hoare P (WHILE b c) (afalse b //\\ P)
  | Hoare_consequence: forall P Q P' Q' c,
      Hoare P c Q ->
      P' -->> P ->
      Q -->> Q' ->
      Hoare P' c Q'.

Quelques règles dérivées.

Lemma Hoare_consequence_pre: forall P P' Q c,
      Hoare P c Q ->
      P' -->> P ->
      Hoare P' c Q.
Proof.
  intros. apply Hoare_consequence with (P := P) (Q := Q); unfold aimp; auto.
Qed.

Lemma Hoare_consequence_post: forall P Q Q' c,
      Hoare P c Q ->
      Q -->> Q' ->
      Hoare P c Q'.
Proof.
  intros. apply Hoare_consequence with (P := P) (Q := Q); unfold aimp; auto.
Qed.

Lemma Hoare_ifthen: forall b c P Q,
    Hoare (atrue b //\\ P) c Q ->
    afalse b //\\ P -->> Q ->
    Hoare P (IFTHENELSE b c SKIP) Q.
Proof.
  intros. apply Hoare_ifthenelse; auto.
  apply Hoare_consequence_pre with Q; auto using Hoare_skip.
Qed.

Un exemple de dérivation.

Example Hoare_swap_xy: forall m n,
  Hoare (aequal (VAR "x") m //\\ aequal (VAR "y") n)
        swap_xy
        (aequal (VAR "x") n //\\ aequal (VAR "y") m).
Proof.
  intros.
  eapply Hoare_consequence_pre.
- unfold swap_xy. eapply Hoare_seq. apply Hoare_assign.
  eapply Hoare_seq. apply Hoare_assign. apply Hoare_assign.
- unfold aequal, aupdate, aand, aimp; cbn. tauto.
Qed.

Exercice (2 étoiles)

Voici une autre manière d'échanger les valeurs de deux variables entières, sans utiliser de variable temporaire.

Definition swap_xy_2 :=
  ASSIGN "x" (PLUS (VAR "x") (VAR "y")) ;;
  ASSIGN "y" (MINUS (VAR "x") (VAR "y")) ;;
  ASSIGN "x" (MINUS (VAR "x") (VAR "y")).

Montrer que ce programme satisfait la même propriété que swap_xy. Indication: reprendre le script de preuve de Hoare_swap_xy, l'adaptation à effectuer est minimale.

Example Hoare_swap_xy_2: forall m n,
  Hoare (aequal (VAR "x") m //\\ aequal (VAR "y") n)
        swap_xy_2
        (aequal (VAR "x") n //\\ aequal (VAR "y") m).
Proof.
  (* A COMPLÉTER *)
Admitted.

4.4. Sûreté de la logique de Hoare


On va interpréter sémantiquement les énoncés Hoare P c Q de la logique de Hoare par la relation triple P c Q ci-dessous, définie en termes de la sémantique naturelle d'IMP (la relation cexec s c s').

Definition triple (P: assertion) (c: com) (Q: assertion) : Prop :=
  forall s s', cexec s c s' -> P s -> Q s'.

Notation "{{ P }} c {{ Q }}" := (triple P c Q) (at level 90, c at next level).

L'interprétation sémantique valide chacune des règles de la logique de Hoare.

Lemma triple_skip: forall P,
     {{P}} SKIP {{P}}.
Proof.
  unfold triple; intros. inversion H; subst. auto.
Qed.

Lemma triple_assign: forall P x a,
      {{aupdate x a P}} ASSIGN x a {{P}}.
Proof.
  unfold triple, aupdate; intros. inversion H; subst. auto.
Qed.

Lemma triple_seq: forall P Q R c1 c2,
      {{P}} c1 {{Q}} ->
      {{Q}} c2 {{R}} ->
      {{P}} c1;;c2 {{R}}.
Proof.
  unfold triple; intros. inversion H1; subst. eauto.
Qed.

Lemma triple_ifthenelse: forall P Q b c1 c2,
      {{atrue b //\\ P}} c1 {{Q}} ->
      {{afalse b //\\ P}} c2 {{Q}} ->
      {{P}} IFTHENELSE b c1 c2 {{Q}}.
Proof.
  unfold triple, aand, atrue, afalse; intros. inversion H1; subst.
  destruct (beval b s) eqn:B; eauto.
Qed.

Lemma triple_while: forall P b c,
      {{atrue b //\\ P}} c {{P}} ->
      {{P}} WHILE b c {{afalse b //\\ P}}.
Proof.
  unfold triple; intros P b c T s s' E. dependent induction E; intros.
- split; auto.
- eapply IHE2; eauto. apply T with s; auto. split; auto.
Qed.

Lemma triple_consequence: forall P Q P' Q' c,
      {{P}} c {{Q}} ->
      P' -->> P ->
      Q -->> Q' ->
      {{P'}} c {{Q'}}.
Proof.
  unfold triple, aimp; intros. eauto.
Qed.

Il s'ensuit que la logique de Hoare est sûre: tout triplet déductible par les règles de la logique est sémantiquement valide.

Theorem Hoare_sound:
  forall P c Q, Hoare P c Q -> {{P}} c {{Q}}.
Proof.
  induction 1; eauto using triple_skip, triple_assign, triple_seq,
  triple_ifthenelse, triple_while, triple_consequence.
Qed.

4.5. Complétude de la logique de Hoare


La réciproque du théorème Hoare_sound est vraie: un "triplet de Hoare" qui est vrai sémantiquement ({{P}} c {{Q}}) peut toujours être dérivé par les règles de Hoare (Hoare P c Q). La démonstration utilise la notion de "plus faible précondition" ("weakest precondition", WP).

La plus faible précondition pour une commande c avec postcondition Q.

Definition wp (c: com) (Q: assertion) : assertion :=
  fun s => forall s', cexec s c s' -> Q s'.

C'est une précondition.

Lemma wp_precondition: forall c Q, {{wp c Q}} c {{Q}}.
Proof.
  unfold triple, wp; intros. auto.
Qed.

C'est la plus faible des préconditions: toute autre précondition l'implique.

Lemma wp_weakest: forall P c Q, {{P}} c {{Q}} -> P -->> wp c Q.
Proof.
  unfold triple, wp, aimp; intros. eauto.
Qed.

Les règles de la logique de Hoare sont suffisamment puissantes pour dériver le fait que wp c Q est une précondition valide pour c et Q.

Lemma Hoare_wp: forall c Q, Hoare (wp c Q) c Q.
Proof.
  induction c; intros Q.
- (* SKIP *)
  eapply Hoare_consequence_pre. apply Hoare_skip.
  unfold aimp, wp; intros. apply H. apply cexec_skip.
- (* ASSIGN *)
  eapply Hoare_consequence_pre. apply Hoare_assign.
  unfold aimp, aupdate, wp; intros. apply H. apply cexec_assign.
- (* SEQ *)
  eapply Hoare_consequence_pre.
  eapply Hoare_seq with (wp c2 Q); eauto.
  unfold aimp, wp; intros. apply H. apply cexec_seq with s'; auto.
- (* IFTHENELSE *)
  apply Hoare_ifthenelse.
  + eapply Hoare_consequence_pre. apply IHc1.
    unfold atrue, aand, aimp, wp; intros. destruct H.
    apply H1. apply cexec_ifthenelse. rewrite H; auto.
  + eapply Hoare_consequence_pre. apply IHc2.
    unfold afalse, aand, aimp, wp; intros. destruct H.
    apply H1. apply cexec_ifthenelse. rewrite H; auto.
- (* WHILE *)
  eapply Hoare_consequence_post.
  + apply Hoare_while.
    eapply Hoare_consequence_pre. apply IHc.
    unfold atrue, aand, aimp, wp; intros. destruct H.
    apply H2. apply cexec_while_loop with s'; auto.
  + unfold afalse, aand, aimp, wp; intros. destruct H.
    apply H0. apply cexec_while_done; auto.
Qed.

Il s'ensuit que tout triplet {{P}} c {{Q}} sémantiquement valide est dérivable par les règles de Hoare.

Theorem Hoare_complete: forall P c Q, {{P}} c {{Q}} -> Hoare P c Q.
Proof.
  intros. apply Hoare_consequence_pre with (wp c Q).
- apply Hoare_wp.
- apply wp_weakest; auto.
Qed.

4.6. Autres règles utiles


Avec la définition sémantique des triplets de Hoare, il est très facile d'ajouter des règles de raisonnement supplémentaires. Ce sont juste des lemmes que l'on démontre une fois pour toute. Par exemple:

Lemma triple_conj:
  forall c P1 Q1 P2 Q2,
  {{P1}} c {{Q1}} -> {{P2}} c {{Q2}} -> {{P1 //\\ P2}} c {{Q1 //\\ Q2}}.
Proof.
  intros; red; intros. destruct H2 as [PRE1 PRE2]. split; eauto.
Qed.

Lemma triple_disj:
  forall c P1 Q1 P2 Q2,
  {{P1}} c {{Q1}} -> {{P2}} c {{Q2}} -> {{P1 \\// P2}} c {{Q1 \\// Q2}}.
Proof.
  intros; red; intros. destruct H2 as [PRE1|PRE2]; [left|right]; eauto.
Qed.

Nous pouvons aussi donner une règle de raisonnement sur l'affectation qui fonctionne "en avant" (la postcondition est déterminée à partir de la précondition) au lieu de "en arrière" comme la règle de Hoare.

Definition aexists {A: Type} (P: A -> assertion) : assertion :=
  fun (s: store) => exists (a: A), P a s.

Lemma triple_assign_fwd: forall x a P,
  {{ P }}
  ASSIGN x a
  {{ aexists (fun m => aexists (fun n =>
     aequal (VAR x) n //\\ aupdate x (CONST m) (P //\\ aequal a n))) }}.
Proof.
  intros. unfold triple, aequal, aupdate; intros.
  inversion H; subst.
  exists (s x); exists (aeval a s); cbn.
  split. apply update_same.
  replace (update x (s x) (update x (aeval a s) s)) with s.
  split; auto.
  apply functional_extensionality; intros y.
  unfold update. destruct (string_dec x y); congruence.
Qed.

Pour finir, nous allons construire une règle d'encadrement ("frame rule" en anglais) qui permet de réutiliser une vérification déjà effectuée de {{P} c {{Q}} pour ajouter des faits supplémentaires R à la précondition et à la postcondition, obtenant une vérification de {{P //\\ R}} c {{Q //\\ R}}.

Par exemple: si on a montré la correction de swap_xy comme suit 
    {{ aequal (VAR "x") m //\\ aequal (VAR "y") n }}
    swap_xy
    {{ aequal (VAR "x") n //\\ aequal (VAR "y") m }}
on devrait pouvoir, sans refaire la vérification de swap_xy, montrer un triplet plus informatif, comme par exemple 
    {{ aequal (VAR "x") m //\\ aequal (VAR "y") n //\\ aequal (VAR "z") p }}
    swap_xy
    {{ aequal (VAR "x") n //\\ aequal (VAR "y") m //\\ aequal (VAR "z") p }}
c'est à dire: "et en plus la valeur de la variable z est préservée".

Ce raisonnement est valide à condition que les faits supplémentaires R portent uniquement sur des variables qui sont pas modifiées pendant l'exécution de la commande c, c'est-à-dire, en première approximation, des variables qui n'apparaissent pas dans une construction ASSIGN de c.

Fixpoint modified_by (c: com) (x: ident) : Prop :=
  match c with
  | SKIP => False
  | ASSIGN y a => x = y
  | SEQ c1 c2 => modified_by c1 x \/ modified_by c2 x
  | IFTHENELSE b c1 c2 => modified_by c1 x \/ modified_by c2 x
  | WHILE b c1 => modified_by c1 x
  end.

Lemma cexec_modified:
  forall x s1 c s2,
  cexec s1 c s2 -> ~modified_by c x -> s2 x = s1 x.
Proof.
  induction 1; cbn; intros MB.
- auto.
- unfold update. destruct (string_dec x0 x); congruence.
- rewrite IHcexec2, IHcexec1 by tauto. auto.
- apply IHcexec. destruct (beval b s); tauto.
- auto.
- rewrite IHcexec2, IHcexec1 by tauto. auto.
Qed.

Syntaxiquement, une assertion P est indépendante d'un ensemble vars de variables si aucune de ces variables n'apparaît dans P. Avec notre codage des assertions comme fonctions store -> Prop, on ne peut pas exprimer cette condition de cette manière. Mais on peut dire que l'assertion prend la même valeur de vérité dans deux états s1 et s2 qui ne diffèrent que par les valeurs des variables dans vars.

Definition independent_of (P: assertion) (vars: ident -> Prop) : Prop :=
  forall s1 s2,
  (forall x, ~ vars x -> s1 x = s2 x) ->
  (P s1 <-> P s2).

Finalement, on obtient la règle d'encadrement suivante.

Lemma triple_frame:
  forall c P Q R,
  {{P}} c {{Q}} ->
  independent_of R (modified_by c) ->
  {{P //\\ R}} c {{Q //\\ R}}.
Proof.
  intros; red; intros. destruct H2 as [PRE1 PRE2]. split.
- eapply H; eauto.
- apply (H0 s' s).
  + intros. apply cexec_modified with c; auto.
  + auto.
Qed.

4.7. Triplets de Hoare forts


La logique de Hoare que nous avons vue jusqu'ici est dite "faible" car elle ne garantit pas la terminaison des programmes, et ne peut donc montrer que des résultats de correction partielle.

En suivant les mêmes approches, nous allons maintenant construire une logique de Hoare "forte", qui garantit la terminaison et montre donc des résultats de correction totale.

Comme nous avons fait pour la logique "faible", nous pourrions donner les règles de la logique "forte" sous forme de prédicat inductif, puis les interpréter sémantiquement. Pour simplifier, nous omettons le prédicat inductif et définissons la logique "forte" directement à partir de la sémantique opérationnelle, via la relation [[P]] c [[Q]] ci-dessous:

Definition Triple (P: assertion) (c: com) (Q: assertion) :=
  forall s, P s -> exists s', cexec s c s' /\ Q s'.

Notation "[[ P ]] c [[ Q ]]" := (Triple P c Q) (at level 90, c at next level).

Notons la différence avec la logique faible:

Les règles de base de la logique forte sont les mêmes que celles de la logique faible, sauf pour les boucles.

Lemma Triple_skip: forall P,
      [[P]] SKIP [[P]].
Proof.
  intros P s PRE. exists s; split; auto. apply cexec_skip.
Qed.

Lemma Triple_assign: forall P x a,
      [[aupdate x a P]] ASSIGN x a [[P]].
Proof.
  intros P x a s PRE. exists (update x (aeval a s) s); split.
- apply cexec_assign.
- exact PRE.
Qed.

Lemma Triple_seq: forall P Q R c1 c2,
      [[P]] c1 [[Q]] -> [[Q]] c2 [[R]] ->
      [[P]] c1;;c2 [[R]].
Proof.
  intros; intros s PRE.
  destruct (H s PRE) as (s1 & EXEC1 & MID).
  destruct (H0 s1 MID) as (s2 & EXEC2 & POST).
  exists s2; split.
- apply cexec_seq with s1; auto.
- exact POST.
Qed.

Lemma Triple_ifthenelse: forall P Q b c1 c2,
      [[atrue b //\\ P]] c1 [[Q]] ->
      [[afalse b //\\ P]] c2 [[Q]] ->
      [[P]] IFTHENELSE b c1 c2 [[Q]].
Proof.
  intros; intros s PRE. destruct (beval b s) eqn:B.
- destruct (H s) as (s' & EXEC & POST). split; auto.
  exists s'; split; auto. constructor; rewrite B; auto.
- destruct (H0 s) as (s' & EXEC & POST). split; auto.
  exists s'; split; auto. constructor; rewrite B; auto.
Qed.

Lemma Triple_consequence: forall P Q P' Q' c,
      [[P]] c [[Q]] -> P' -->> P -> Q -->> Q' ->
      [[P']] c [[Q']].
Proof.
  intros; intros s PRE.
  destruct (H s) as (s' & EXEC & POST). apply H0; auto.
  exists s'; auto.
Qed.

Pour les boucles WHILE b c, le triplet fort doit garantir la terminaison de la boucle pour tous les états initiaux satisfaisant la précondition. Une manière simple de garantir la terminaison est d'exhiber une "variante": une expression à valeurs entières qui décroît strictement à chaque tour de boucle tout en restant positive.

Definition alessthan (a: aexp) (v: Z) : assertion :=
  fun (s: store) => 0 <= aeval a s < v.

Lemma Triple_while: forall P variant b c,
  (forall v,
     [[ P //\\ atrue b //\\ aequal variant v ]]
     c
     [[ P //\\ alessthan variant v ]])
  ->
     [[P]] WHILE b c [[P //\\ afalse b]].
Proof.
  intros P variant b c T.
  assert (REC: forall v s, P s -> aeval variant s = v ->
               exists s', cexec s (WHILE b c) s' /\ (P s' /\ beval b s' = false)).
  { induction v using (well_founded_induction (Z.lt_wf 0)).
    intros. destruct (beval b s) eqn:B.
  - destruct (T v s) as (s1 & EXEC1 & (PS1 & LT1)). unfold aand, aequal, atrue; auto.
    destruct (H _ LT1 s1 PS1) as (s2 & EXEC2 & PS2). auto.
    exists s2; split; auto. apply cexec_while_loop with s1; auto.
  - exists s; split; auto. apply cexec_while_done; auto.
  }
  intros s PRE. apply REC with (v := aeval variant s); auto.
Qed.

Exercice (3 étoiles)


La technique de la "variante" et l'ordre sur les entiers positifs ne suffisent pas toujours à montrer la terminaison d'une boucle WHILE. Voici une règle qui utilise deux variantes et l'ordre lexicographique entre paires d'entiers positifs. Montrer que cette règle est valide.

Lemma Triple_while_lexico: forall P variant1 variant2 b c,
  (forall v1 v2,
    [[ P //\\ atrue b //\\ aequal variant1 v1 //\\ aequal variant2 v2 ]]
    c
    [[ P //\\ (alessthan variant1 v1 \\// aequal variant1 v1 //\\ alessthan variant2 v2) ]])
  ->
    [[P]] WHILE b c [[P //\\ afalse b]].
Proof.
  intros P variant1 variant2 b c T.
  assert (REC: forall v1 v2 s, P s -> aeval variant1 s = v1 -> aeval variant2 s = v2 ->
               exists s', cexec s (WHILE b c) s' /\ (P s' /\ beval b s' = false)).
  (* A COMPLÉTER *)
Admitted.

4.8. Génération des conditions de vérification


Exceptée la règle pour les boucles WHILE, les règles de la logique de Hoare peuvent se lire comme un algorithme qui, étant données une commande c et une postcondition Q, calcule une plus faible précondition P. Par exemple, si c se compose de deux affectations en séquence 
    c = ASSIGN x1 a1 ;; ASSIGN x2 a2
la précondition P est déterminée comme 
    P = aupdate x1 a1 (aupdate x2 a2 Q)
Un tel calcul est beaucoup plus simple qu'une recherche de preuve générale, cette dernière pouvant faire intervenir la règle d'affaiblissement triple_consequence à tout moment.

Le problème est bien entendu les boucles WHILE. L'invariant de la boucle ne peut pas être déterminé automatiquement par calcul.

Dans ce qui suit, nous développons une approche hybride où les boucles sont annotées manuellement par leurs invariants de boucle, mais où toutes les autres préconditions sont calculées automatiquement à partir des postconditions.

Module VCGEN.

Voici le langage des commandes avec les boucles WHILE annotées par un invariant Inv.

Inductive com: Type :=
  | SKIP
  | ASSIGN (x: ident) (a: aexp)
  | SEQ (c1: com) (c2: com)
  | IFTHENELSE (b: bexp) (c1: com) (c2: com)
  | WHILE (Inv: assertion) (b: bexp) (c1: com). (* nouveau! *)

La fonction pre c Q calcule une précondition pour la commande c et la postcondition Q, par "exécution en arrière" de la commande c et application des règles de la logique de Hoare. Seule exception: pour les boucles WHILE, on prend l'invariant déclaré pour la boucle comme précondition.

Fixpoint pre (c: com) (Q: assertion) : assertion :=
  match c with
  | SKIP => Q
  | ASSIGN x a => aupdate x a Q
  | SEQ c1 c2 => pre c1 (pre c2 Q)
  | IFTHENELSE b c1 c2 => atrue b //\\ pre c1 Q \\// afalse b //\\ pre c2 Q
  | WHILE Inv b c => Inv
  end.

Le triplet de Hoare {{ pre c Q }} c {{ Q }} n'est pas toujours vrai: il faut aussi s'assurer que les invariants déclarés pour les boucles sont bien des invariants. Pour une boucle WHILE Inv b c de postcondition Q, il faut que La fonction vcg (Verification Condition Generator) ci-dessous collecte ces "conditions de vérification" pour toutes les boucles WHILE apparaissant dans la commande c.

Fixpoint vcg (c: com) (Q: assertion) : Prop :=
  match c with
  | SKIP => True
  | ASSIGN x a => True
  | SEQ c1 c2 => vcg c1 (pre c2 Q) /\ vcg c2 Q
  | IFTHENELSE b c1 c2 => vcg c1 Q /\ vcg c2 Q
  | WHILE Inv b c =>
       vcg c Inv
    /\ (afalse b //\\ Inv -->> Q)
    /\ (atrue b //\\ Inv -->> pre c Inv)
  end.

Le triplet {{P}} c {{Q}} est valide dès lors que

Definition vcgen (P: assertion) (c: com) (Q: assertion) : Prop :=
  (P -->> pre c Q) /\ vcg c Q.

Pour montrer la correction de cet algorithme de vérification, nous définissons l'effacement erase c d'une commande annotée en commande IMP standard. Il s'agit juste d'oublier les invariants de boucles qui annotent les noeuds WHILE.

Fixpoint erase (c: com) : IMP.com :=
  match c with
  | SKIP => IMP.SKIP
  | ASSIGN x a => IMP.ASSIGN x a
  | SEQ c1 c2 => IMP.SEQ (erase c1) (erase c2)
  | IFTHENELSE b c1 c2 => IMP.IFTHENELSE b (erase c1) (erase c2)
  | WHILE Inv b c => IMP.WHILE b (erase c)
  end.

Nous pouvons alors montrer que pre c Q est une précondition valide de c et de Q, pourvu que les conditions vcg c Q soient vraies.

Lemma vcg_sound:
  forall c Q, vcg c Q -> {{pre c Q}} erase c {{Q}}.
Proof.
  induction c; cbn; intros.
- apply triple_skip.
- apply triple_assign.
- destruct H as (V1 & V2).
  apply triple_seq with (pre c2 Q); auto.
- destruct H as (V1 & V2).
  apply triple_ifthenelse.
  + eapply triple_consequence. eapply IHc1; eauto.
    unfold aimp, aand, aor, atrue, afalse. intuition congruence.
    unfold aimp; auto.
  + eapply triple_consequence. eapply IHc2; eauto.
    unfold aimp, aand, aor, atrue, afalse. intuition congruence.
    unfold aimp; auto.
- destruct H as (V1 & V2 & V3).
  eapply triple_consequence.
  + apply triple_while. eapply triple_consequence. apply IHc; eauto.
    eauto. red; auto.
  + red; auto.
  + auto.
Qed.

On en déduit la correction de l'algorithme vcgen.

Theorem vcgen_correct:
  forall P c Q, vcgen P c Q -> {{P}} erase c {{Q}}.
Proof.
  unfold vcgen; intros. destruct H as (V1 & V2).
  eapply triple_consequence. eapply vcg_sound; eauto. auto. red; auto.
Qed.

Application: la division Euclidienne


Infix ";;" := SEQ (at level 80, right associativity).

Voici la précondition, l'invariant de boucle, et la postcondition pour le programme de division euclidienne par soustraction itérée.

Definition Pre (s: store) :=
  s "a" >= 0 /\ s "b" > 0.

Definition Inv (s: store) :=
  s "r" >= 0 /\ s "b" > 0 /\ s "a" = s "b" * s "q" + s "r".

Definition Post (s: store) :=
  s "q" = s "a" / s "b" /\ s "r" = s "a" mod s "b".

Voici le programme IMP avec la boucle annotée par Inv.

Definition Euclidean_division :=
  ASSIGN "r" (VAR "a") ;;
  ASSIGN "q" (CONST 0) ;;
  WHILE Inv (LESSEQUAL (VAR "b") (VAR "r"))
    (ASSIGN "r" (MINUS (VAR "r") (VAR "b")) ;;
     ASSIGN "q" (PLUS (VAR "q") (CONST 1))).

Et voici la preuve de sa correction. Elle n'applique explicitement aucune des règles de la logique de Hoare. À la place, on applique le théorème vcgen_correct, puis on fait calculer par Coq les conditions de vérification. Il reste une formule de logique usuelle à démontrer, en utilisant les tactiques Coq standard.

Theorem Euclidean_division_correct:
  {{Pre}} erase Euclidean_division {{Post}}.
Proof.
  apply vcgen_correct. red; cbn.
  unfold aimp, aupdate, aand, afalse, atrue, Pre, Post, Inv; cbn.
  intuition auto.
  (* La précondition implique l'invariant de boucle. *)
  - lia.
  (* L'invariant et la sortie de boucle impliquent la postcondition. *)
  - apply Z.leb_gt in H0. apply Zdiv_unique with (s "r"). lia. auto.
  - apply Z.leb_gt in H0. apply Zmod_unique with (s "q"). lia. auto.
  (* L'invariant de boucle est préservé *)
  - apply Z.leb_le in H0. lia.
  - lia.
Qed.

Exercice (1 étoile)

Refaire la vérification en supprimant l'hypothèse s "b" > 0 de la précondition et de l'invariant. Comment est-il possible que la vérification "passe" même quand le diviseur b est nul?

Exercice (3 étoiles)

Spécifier et vérifier le programme suivant. Il met dans r la racine carrée entière de a. 
    r := 0; s := 1;
    while s <= a do (r := r + 1; s := s + r + r + 1)

End VCGEN.
Generated by coq2html