Library GCContinuity

Continuity of the wp predicate for GC

Require Import Facts States.
Require Import GCSemantics.
Set Implicit Arguments.

Module GCContinuity (Sigma : State).
Module GCSem := GCSemantics.GCSemantics Sigma.
Export GCSem.

Implicit Types (G : gc) (P Q:Pred state) (x:state) (n:nat).


Lemma gc_continuous´ :
  ( s, continuous (wpg^~ s))
  ( G, continuous (fun Q xG xwpG Q G x)).

Theorem gc_continuous s : continuous (wpg^~ s).

Equivalence to Dijkstra's definition of WP

Fixpoint dijkstra_wpg Q s : Pred state :=
  match s with
  | SkipQ
  | Assn aQ \o a
  | Seq s tdijkstra_wpg (dijkstra_wpg Q t) s
  | Case Gfun xgtest G x wpG´ dijkstra_wpg Q G x
  | Do G
    let F P x :=
        ((G:gc) x wpG´ dijkstra_wpg P G x) (~~(G:gc) x Q x)
    in fixk F

Lemma wpG_continuous G (Q : NPred state) x :
  G xchain QwpG (sup Q) G x m, wpG (Q m) G x.

Theorem dijkstra_equiv :
  ( s Q x, wpg Q s x dijkstra_wpg Q s x)
  ( G Q x, wpG Q G x wpG´ dijkstra_wpg Q G x).

End GCContinuity.