NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library sgoto_hoare

Require Import ssreflect ssrbool.
Require Import Arith_ext Lists_ext.
Require while.
Require Import goto sgoto.

Hoare Logic of SGoto





This corresponds to Section 3.2 of [Saabas&Uustalu2007]. The type assert was defined in the module for the While language.

Module SGoto_Hoare (while_hoare_deter_m : while.WHILE_HOARE_DETER).

Module Import sgoto_m := SGoto while_hoare_deter_m.
Import goto_deter_m.
Import goto_m.
Import while_hoare_deter_m.


Definition assn := label -> assert.

Local Open Scope while_assert_scope.

Definition restrict (P : assn) d : assn := fun l => P l //\\ (fun _ _ => In l d).

Definition restrict_cplt (P : assn) d : assn := fun l => while.Not (fun _ _ => In l d) //\\ P l.

Lemma restrict_dom : forall l d (P : assn) s h, In l d -> P l s h -> restrict P d l s h.

Lemma restrict_cplt_dom : forall (P : assn) l s h d, P l s h -> ~ In l d -> restrict_cplt P d l s h.

Reserved Notation "'[^' P '^]' c '[^' Q '^]'" (at level 82, no associativity).


Figure 3 (Hoare rules of SGoto) in [Saabas&Uustalu2007].

Local Open Scope sgoto_scope.

Notation "'_assn'" := assn : sgoto_hoare_scope. Local Open Scope sgoto_hoare_scope.

Inductive hoare_sgoto : assn -> scode -> assn -> Prop :=
| hoare_cmd : forall l c P,
  [^ fun pc => fun s h => pc = l /\ (wp0 c (P (S l))) s h \/ pc <> l /\ P pc s h ^]
     sC l c [^ P ^]
| hoare_jmp : forall l j Q,
  [^ fun pc => fun s h => pc = l /\ (Q j s h \/ j = l) \/ pc <> l /\ Q pc s h ^]
     sB l (jmp j) [^ Q ^]
| hoare_branch : forall l b j Q,
  [^ fun pc => fun s h =>
     pc = l /\ (~~ eval_b b (s, h) /\ Q (S l) s h \/ eval_b b (s, h) /\ ( Q j s h \/ j = l)) \/
     pc <> l /\ Q pc s h ^]
     sB l (cjmp b j) [^ Q ^]
| hoare_sO : forall P, [^ P ^] sO [^ P ^]
| hoare_sS : forall sc0 sc1 P,
  [^ restrict P (sdom sc0) ^] sc0 [^ P ^] -> [^ restrict P (sdom sc1) ^] sc1 [^ P ^] ->
  [^ P ^] sc0 [+] sc1 [^ restrict_cplt P (sdom (sc0 [+] sc1)) ^]
| hoare_sgoto_conseq : forall sc (P Q P' Q': assn),
  (forall l, P l ===> P' l) -> (forall l, Q' l ===> Q l) ->
  [^ P' ^] sc [^ Q' ^] -> [^ P ^] sc [^ Q ^]
where "'[^' P '^]' c '[^' Q '^]'" := (hoare_sgoto P c Q) : sgoto_hoare_scope.

Theorem 10 (Soundness) in [Saabas&Uustalu2007]:

Module while_semop_prop_m := while.While_Semop_Prop while_hoare_deter_m.

Lemma hoare_sgoto_sound : forall sc P Q, [^ P ^] sc [^ Q ^] ->
  forall l s h, P l s h -> ~ (Some (l, (s, h)) >- sc ---> None) /\
    forall l' s' h', Some (l, (s, h)) >- sc ---> Some (l', (s', h')) -> Q l' s' h'.

The semantic definition of the weakest precondition from [Saabas&Uustalu2007]. The additional conjunct is to take errors into account.

Definition wlp_semantics (sc : scode) (Pi : assn) : assn := fun l s h =>
  ~ (Some (l, (s, h)) >- sc ---> None) /\
  forall l' s' h', Some (l, (s, h)) >- sc ---> Some (l', (s', h')) -> Pi l' s' h'.

Lemma 11 in [Saabas&Uustalu2007]:

Lemma wlp_completeness : forall sc (Hwf : wellformed sc) Q, [^ wlp_semantics sc Q ^] sc [^ Q ^].

Theorem 12 (Completeness) in [Saabas&Uustalu2007].

Lemma hoare_sgoto_complete : forall (P Q : assn) sc (Hwf : wellformed sc),
  (forall l s h, P l s h ->
    ~ Some (l, (s, h)) >- sc ---> None /\
    (forall l' s' h', Some (l,(s,h)) >- sc ---> Some (l',(s',h')) -> Q l' s' h')) ->
  [^ P ^] sc [^ Q ^].

End SGoto_Hoare.