Library Scat.Concrete

Syntax and semantics of concrete programming language


Require Export Atoms.

Abstract syntax of statements


Inductive prog: Type :=

 
atomic statement
 | iat (inst: atom)

 
sequence of statements
 | seq (pf pn:prog)

 
non-determinitic choice
 | join (pl pr:prog)
 
 
loop (with non-deterministic stop)
 | loop (body:prog).

Notations
Bind Scope prog_scope with prog.
Delimit Scope prog_scope with prog.

Notation "p1 -; p2" := (seq p1 p2)
  (at level 95, right associativity): prog_scope.

Coercion iat: atom >-> prog.

Open Scope prog_scope.

Notation "'ifc' c 'then' p1 'else' p2 'fi'" :=(join (ensure c -; p1) (ensure (not c) -; p2))
   (at level 95): prog_scope.

Notation "'while' c 'do' p 'done'" := (loop (ensure c -; p) -; ensure (not c))
   (at level 95): prog_scope.

Big step semantics with an error state (for require)

Inductive sem: progstateoption stateProp :=
 | sem_iat inst s s0:
     asem inst s s0sem (iat inst) s s0
 | sem_seq pf pn s0 s1 s2:
     sem pf s0 (Some s1)
     → sem pn s1 s2
     → sem (pf -; pn) s0 s2
 | sem_seq_ko pf pn s:
     sem pf s None
     → sem (pf -; pn) s None
 | sem_join_l pl pr s0 s1:
     sem pl s0 s1
     → sem (join pl pr) s0 s1
 | sem_join_r pl pr s0 s1:
     sem pr s0 s1
     → sem (join pl pr) s0 s1
 | sem_loop_stop body s:
     sem (loop body) s (Some s)
 | sem_loop_continue body s0 s1 s2:
     sem body s0 (Some s1)
      → sem (loop body) s1 s2
     → sem (loop body) s0 s2
 | sem_loop_ko body s :
     sem body s None
       → sem (loop body) s None.

Hint Resolve sem_iat sem_seq sem_seq_ko sem_join_l sem_join_r sem_loop_stop sem_loop_continue sem_loop_ko: sem.

Definition is_ok (p: prog) := s s', sem p s s's' None.

Predicate Transformers Semantics of concrete language


Fixpoint wlp (p: prog) (post: stateProp) (s:state) : Prop :=
  match p with
 | iat instawlp inst post s
 | seq pf pnwlp pf (wlp pn post) s
 | join pl pr(wlp pl post s) (wlp pr post s)
 | loop body
     inv: stateProp,
        (inv s)
      ( s', inv s'wlp body inv s')
      ( s', inv s'post s')
 end.

Lemma wlp_monotonic p:
   (P Q: stateProp) s, wlp p P s
    ( s, P sQ s) → wlp p Q s.
Proof.
  induction p; simpl; intuition simpl; eauto with echecker.
  firstorder.
Qed.

Hint Resolve wlp_monotonic: echecker.

Theorem wlp_correctness p s s': (sem p s s') → post, wlp p post sok s' post.
Proof.
  induction 1; simpl in × |- *; intuition eauto with echecker.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
Qed.

Lemma wlp_isok p: ( s, wlp p (fun _True) s) → is_ok p.
Proof.
  unfold is_ok. intros H s s' H0 H1; subst.
  exact (wlp_correctness _ _ _ H0 _ (H s)).
Qed.

Theorem wlp_complete p: post s, ( s', sem p s s'ok s' post) → wlp p post s.
Proof.
  induction p; simpl in × |- *; intuition eauto with sem echecker.
  intros; eapply awlp_complete. eauto with sem.
  eapply wlp_monotonic.
  eapply IHp1.
  2: intros s0 H0; eapply IHp2; pattern s0; eapply H0.
  intros s'; case s'; simpl; intros; eauto with sem.
  case (H None); eauto with sem.
  constructor 1 with (x:=fun s s', sem (loop p) s s'ok s' post).
  constructor 1.
  eauto with echecker sem.
  constructor 1; intros s' H0.
  eapply wlp_monotonic.
  eapply IHp.
  2: intros s1 H1; pattern s1; apply H1.
  intros s1; case s1; simpl; intros; eauto with sem.
  case (H0 None); eauto with sem.
  apply (H0 (Some s')). eauto with sem.
Qed.

Lemma isok_wlp p s: is_ok pwlp p (fun _True) s.
Proof.
  unfold is_ok; intros; apply wlp_complete.
  intros s'; case s'; simpl; firstorder.
Qed.

Normalization of bracketing


Definition seq_outskip (pf pn: prog): prog :=
  match pn with
  | skippf
  | _pf -; pn
  end.

normalize_rec pf pn = normalization of seq pf pn under the hypothesis that pn is normalized.
Fixpoint normalize_rec (pf pn: prog): prog :=
  match pf with
  | seq pf' pn'normalize_rec pf' (normalize_rec pn' pn)
  | join pl prseq_outskip (join (normalize_rec pl skip) (normalize_rec pr skip)) pn
  | loop bodyseq_outskip (loop (normalize_rec body skip)) pn
  | skippn
  | iat instseq_outskip inst pn
 end.

Definition normalize p := normalize_rec p skip.

Lemma wlp_seq_outskip_fwd pf:
   pn (P: stateProp) s, wlp pf (wlp pn P) swlp (seq_outskip pf pn) P s.
Proof.
  intros pn; case pn; simpl; eauto with checker echecker.
  intros inst; case inst; simpl; eauto with echecker.
Qed.
Hint Resolve wlp_seq_outskip_fwd: checker.

Lemma wlp_normalize_rec_fwd pf:
    pn (P: stateProp) s, (wlp pf (wlp pn P) s) → (wlp (normalize_rec pf pn) P s).
Proof.
  induction pf; simpl; try (intuition eauto with checker echecker; fail); intros pn P s H.
  generalize H; clear H; case inst; simpl; intros; eauto with checker.
  apply wlp_seq_outskip_fwd; simpl.
  intuition eauto with echecker.
  apply wlp_seq_outskip_fwd; simpl.
  case H; clear H.
  intros invariant; intuition.
  constructor 1 with (x:=invariant).
  intuition eauto with echecker.
Qed.

Lemma normalize_fwd_correctness p:
    (P: stateProp) s, (wlp p P s) → (wlp (normalize p) P s).
Proof.
  unfold normalize; intros; apply wlp_normalize_rec_fwd. simpl; eauto with echecker.
Qed.

Lemma wlp_seq_outskip_bck pf:
   pn (P: stateProp) s, wlp (seq_outskip pf pn) P swlp pf (wlp pn P) s.
Proof.
  intros pn; case pn; simpl; eauto with checker echecker.
  intros inst; case inst; simpl; eauto with echecker.
Qed.
Hint Resolve wlp_seq_outskip_bck: checker.

Lemma wlp_normalize_rec_bck pf:
    pn (P: stateProp) s, (wlp (normalize_rec pf pn) P s) → (wlp pf (wlp pn P) s).
Proof.
  induction pf; try (simpl; intuition eauto with checker echecker; fail).
  intros pn P s H; apply wlp_seq_outskip_bck. generalize H; clear H; case inst; simpl; auto with checker.
  simpl; intros pn P s H. generalize (wlp_seq_outskip_bck _ _ _ _ H); simpl.
  intuition eauto with echecker.
  simpl; intros pn P s H. generalize (wlp_seq_outskip_bck _ _ _ _ H); simpl.
  firstorder.
Qed.

Lemma normalize_bck_correctness p:
    (P: stateProp) s, (wlp (normalize p) P s) → (wlp p P s).
Proof.
  unfold normalize; intros; eapply wlp_monotonic.
  eapply wlp_normalize_rec_bck; eauto.
  simpl; auto.
Qed.

Syntactic Equality of programs


Fixpoint prog_eq (p1 p2: prog) : bool :=
 match p1,p2 with
 | iat inst1, iat inst2atom_eq inst1 inst2 &&& true
 | seq pf1 pn1, seq pf2 pn2
    prog_eq pf1 pf2 &&& prog_eq pn1 pn2
 | join pl1 pr1, join pl2 pr2
    prog_eq pl1 pl2 &&& prog_eq pr1 pr2
 | loop body1, loop body2
    prog_eq body1 body2
 | _,_false
 end.

Lemma prog_eq_wlp p1 p2: post s, prog_eq p1 p2=truewlp p1 post swlp p2 post s.
Proof.
  decide_eqb_eq p1 p2; eqtrue.
  intros; eauto with eqtrue.
  intros; eauto with echecker.
  intuition.
  firstorder.
Qed.

Lemma prog_eq_normalize_wlp p1 p2: post s, prog_eq (normalize p1) (normalize p2)=truewlp p1 post swlp p2 post s.
Proof.
  intros; apply normalize_bck_correctness.
  eapply prog_eq_wlp; eauto.
  apply normalize_fwd_correctness.
  auto.
Qed.

Lemma prog_eq_isok p1 p2: prog_eq (normalize p1) (normalize p2) = trueis_ok p1is_ok p2.
Proof.
  intros; apply wlp_isok.
  intros; eapply prog_eq_normalize_wlp; eauto.
  apply isok_wlp; auto.
Qed.