# Semantics of GC

We give an inductive axiomatic semantics to GC, and characterize weakest preconditions with a recursive function. We show the equivalence of both formulations.
Require Import Facts States GCSyntax.
Set Implicit Arguments.

Module GCSemantics (Sigma : State).
Module GCSyn := GCSyntax.GCSyntax Sigma.
Export GCSyn.

Implicit Types (P Q : Pred state) (x y z : state).
Implicit Types (a : action) (b : guard) (G : gc) (s t : cmd).

Test if any guard is true.

Definition gtest G : statebool :=
fun xhas (fun p : guardp x) (unzip1 G).
Coercion gtest : gc >-> Funclass.

## Axiomatic Semantics

Inductive wps Q : cmdPred state :=
| wps_skip x :
Q x
wps Q Skip x
| wps_assn a x :
Q (a x) →
wps Q (Assn a) x
| wps_seq s t x P :
wps P s x
P <<= wps Q t
wps Q (Seq s t) x
| wps_case G x :
G x
( b s, (b,s) \in Gb xwps Q s x) →
wps Q (Case G) x
| wps_loop_true G x P :
G x
( b s, (b,s) \in Gb xwps P s x) →
P <<= wps Q (Do G) →
wps Q (Do G) x
| wps_loop_false G x :
~~G x
Q x
wps Q (Do G) x.

## WP Semantics

Definition wpG´ (wp : Pred statecmdPred state) Q : gcPred state :=
fix rec G x := match G with
| (b,s) :: G(b xwp Q s x) rec G x
| [::]True
end.

Fixpoint wpg Q s : Pred state :=
match s with
| SkipQ
| Assn aQ \o a
| Seq s twpg (wpg Q t) s
| Case Gfun xgtest G x wpG´ wpg Q G x
| Do GFix (fun P xif gtest G x then wpG´ wpg P G x else Q x)
end.

Notation wpG := (wpG´ wpg).

## Equivalence of axiomatic and wp semantics

Lemma gtest_cons (G : gc) b s x :
gtest ((b,s) :: G) x = b x || G x.

Lemma gtestP (G : gc) x :
reflect ( (b:guard) (s:cmd), (b,s) \in G b x) (G x).

Lemma gtest_contra (G : gc) b s x :
(b,s) \in G~~G x~~b x.

Lemma wpgG_mono :
( s, monotone (wpg^~ s)) ( G, monotone (wpG^~ G)).

Lemma wpg_mono s : monotone (wpg^~ s).
Lemma wpG_mono G : monotone (wpG^~ G).

Lemma wpgG_wps :
( s Q, wpg Q s <<= wps Q s)
( G Q x,
wpG Q G x b s, (b,s) \in Gb xwps Q s x).

Lemma wpg_wps Q s : wpg Q s <<= wps Q s.

Lemma wps_wpG Q (G:gc) x :
( b s, (b,s) \in Gb xwpg Q s x) →
wpG Q G x.

Lemma wps_wpg Q (s : cmd) : wps Q s <<= wpg Q s.

End GCSemantics.