Library Scat.Atoms

Syntax and semantics of atomic statements.

They are shared by concrete and abstract (kernel)

Require Export Conditions.
Require Import Classical_Prop.

Abstract syntax of atomic statements.


Inductive atom: Type :=

 
non-deterministic assignment
 | guassign (l:list var) (post: cond)

 
do nothing
 | skip

 
require a precondition pre mesg prints as a comment in VC
 | xrequire (pre: cond) (mesg: string)

 
ensure a postcondition post (e.g. a guard)
 | ensure (post: cond)

 
deterministic assignment
 | assign (x: var) (t: term).

require with empty mesg
Definition require (pre: cond) := xrequire pre "".

Semantics of atoms

Inductive asem: atomstateoption stateProp :=
 | asem_guassign l post s0 s1:
     lframeeq l s0 s1oeval post s0 s1asem (guassign l post) s0 (Some s1)
 | asem_skip s:
     asem skip s (Some s)
 | asem_req_ok c m s:
     eval c s
     → asem (xrequire c m) s (Some s)
 | asem_req_ko c m s:
     ~(eval c s)
     → asem (xrequire c m) s None
 | asem_ensure c s:
     eval c s
     → asem (ensure c) s (Some s)
 | asem_assign x t s:
     asem (assign x t) s (Some (add (vid x) (teval t s) s)).

Hint Resolve Some asem_guassign asem_skip asem_req_ok asem_req_ko asem_ensure asem_assign: sem.

Semantics by wlp


Definition awlp (p: atom) (post: stateProp) (s:state) : Prop :=
 match p with
 | guassign l c s', lframeeq l s s'oeval c s s'post s'
 | skippost s
 | xrequire c meval c s post s
 | ensure c ⇒ (eval c s) → (post s)
 | assign x tpost (add (vid x) (teval t s) s)
 end.

Lemma awlp_monotonic p:
   (P Q: stateProp) s, awlp p P s
    ( s, P sQ s) → awlp p Q s.
Proof.
  destruct p; simpl; intuition simpl; eauto.
Qed.

Hint Resolve ok_monotonic awlp_monotonic: echecker.

Lemma awlp_correctness p s s': (asem p s s') → post, awlp p post sok s' post.
Proof.
  destruct 1; simpl in × |- *; intuition eauto with echecker.
Qed.

Hint Resolve awlp_correctness: echecker.

Lemma awlp_complete p: post s, ( s', asem p s s'ok s' post) → awlp p post s.
Proof.
  destruct p; simpl in × |- *; intros; try (refine (H (Some _) _); eauto with sem).
  case (classic (eval pre s)).
  intuition refine (H (Some _) _); eauto with sem.
  intros; case (H None). eauto with sem.
Qed.

Syntactic equality (necessary on "concrete" atoms only)


Definition atom_eq (inst1 inst2: atom) :=
  match inst1, inst2 with
  | guassign l1 post1, guassign l2 post2lvar_eq l1 l2 &&& cond_eq post1 post2
  | skip, skiptrue
  | xrequire pre1 _, xrequire pre2 _cond_eq pre1 pre2
  | ensure post1, ensure post2cond_eq post1 post2
  | assign x1 t1, assign x2 t2var_eq x1 x2 &&& term_eq t1 t2
  | _, _false
  end.

Lemma atom_eq_awlp (inst1 inst2: atom) post s: atom_eq inst1 inst2=trueawlp inst1 post sawlp inst2 post s.
Proof.
  decide_eqb_eq inst1 inst2; eqtrue.
  intros H1 H2 s' H3 H4.
  apply H2.
  eapply lvar_eq_lframeeq; eauto.
  erewrite cond_eq_oeval; eauto.
  intuition.
  erewrite <- cond_eq_eval; eauto.
  intros H0 H1 H2; apply H1.
  erewrite cond_eq_eval; eauto.
  intros; erewrite <- var_eq_eq; eauto.
  erewrite <- term_eq_eval; eauto.
Qed.

Hint Resolve atom_eq_awlp: eqtrue.

angel_awlp angelic wlp, e.g. an "angelic" interpretation of non-determinism,

See refinement calculus. This is used for abstraction of concrete terms

Definition angel_awlp (p: atom) (post: stateProp) (s:state) : Prop :=
 match p with
 | guassign l c s', lframeeq l s s' oeval c s s' post s'
 | skippost s
 | xrequire c m ⇒ (eval c s) → post s
 | ensure c(eval c s) (post s)
 | assign x tpost (add (vid x) (teval t s) s)
 end.

Lemma angel_awlp_monotonic p:
   (P Q: stateProp) s, angel_awlp p P s
    ( s, P sQ s) → angel_awlp p Q s.
Proof.
  destruct p; simpl; firstorder.
Qed.

Lemma angel_awlp_duality p P s: angel_awlp p P s~(awlp p (fun s~(P s)) s).
Proof.
  destruct p; simpl; firstorder.
Qed.

Hint Resolve angel_awlp_monotonic angel_awlp_duality: angel.