Changeset 20


Ignore:
Timestamp:
Aug 19, 2010, 12:36:03 PM (8 years ago)
Author:
campbell
Message:

Add resumption monad based version of the executable semantics with simple I/O.

Location:
C-semantics
Files:
5 added
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Cexec.ma

    r17 r20  
    865865nwhd; napply (star_step … IH); //;
    866866nqed.
     867
     868nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) :
     869 res (trace×state) ≝
     870match is_final_state s with
     871[ inl _ ⇒ OK ? 〈E0, s〉
     872| inr _ ⇒
     873  match n with
     874  [ O ⇒ OK ? 〈E0, s〉
     875  | S n' ⇒
     876      〈t,s'〉 ← exec_step ge s;:
     877      〈t',s''〉 ← exec_steps_without_proof n' ge s';:
     878      OK ? 〈t ⧺ t',s''〉
     879  ]
     880].
  • C-semantics/Smallstep.ma

    r3 r20  
    461461Variable final_state1: state1 -> int -> Prop.
    462462Variable ge1: genv1.
    463 
     463*)
     464
     465nrecord semantics : Type[1] ≝
     466{ trans :> transrel
     467; initial : (state trans) → Prop
     468; final : (state trans) → int → Prop
     469; ge : (genv trans)
     470}.
     471
     472(*
    464473(** The second small-step semantics is also axiomatized. *)
    465474
     
    486495  final_state1 st1 r ->
    487496  final_state2 st2 r.
    488 
     497*)
     498
     499nrecord related_semantics : Type[1] ≝
     500{ sem1 : semantics
     501; sem2 : semantics
     502; match_states : state sem1 → state sem2 → Prop
     503; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
     504; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r
     505}.
     506
     507(*
    489508(** Simulation when one transition in the first program
    490509    corresponds to zero, one or several transitions in the second program.
     
    508527  (plus step2 ge2 st2 t st2' \/ (star step2 ge2 st2 t st2' /\ order st1' st1))
    509528  /\ match_states st1' st2'.
    510 
    511 Lemma simulation_star_star:
    512   forall st1 t st1', star step1 ge1 st1 t st1' ->
    513   forall st2, match_states st1 st2 ->
    514   exists st2', star step2 ge2 st2 t st2' /\ match_states st1' st2'.
    515 Proof.
    516   induction 1; intros.
    517   exists st2; split. apply star_refl. auto.
    518   destruct (simulation H H2) as [st2' [A B]].
    519   destruct (IHstar _ B) as [st3' [C D]].
    520   exists st3'; split; auto.
    521   apply star_trans with t1 st2' t2; auto.
    522   destruct A as [F | [F G]].
    523   apply plus_star; auto.
    524   auto.
    525 Qed.
    526 
     529*)
     530nrecord order_sim : Type[1] ≝
     531{ sem :> related_semantics
     532; order : state (sem1 sem) → state (sem1 sem) → Prop
     533(* ; order_wf  ? *)
     534; simulation : ∀st1,t,st1'. step (sem1 sem) (ge (sem1 sem)) st1 t st1' →
     535               ∀st2. match_states sem st1 st2 →
     536               ∃st2'. (plus (sem2 sem) (ge (sem2 sem)) st2 t st2' ∨               
     537                       (star (sem2 sem) (ge (sem2 sem)) st2 t st2' ∧
     538                        order st1' st1))
     539                      ∧ match_states sem st1' st2'
     540}.
     541
     542nlemma simulation_star_star: ∀sim:order_sim.
     543  ∀st1,t,st1'. star (sem1 sim) (ge (sem1 sim)) st1 t st1' →
     544  ∀st2. match_states sim st1 st2 →
     545  ∃st2'. star (sem2 sim) (ge (sem2 sim)) st2 t st2' ∧ match_states sim st1' st2'.
     546#sim st1 t st1' H; nelim H;
     547##[ #st1'' st2 Hmatch;
     548    @ st2; @; //;
     549##| #st1 tA st1A tB st1B t Hstep Hstar Ht IH st2 Hmatch;
     550    nelim (simulation sim ??? Hstep ? Hmatch); #st2'; *; #A B;
     551    nelim (IH ? B); #st3'; *; #C D;
     552    @ st3'; @; //;
     553    napply (star_trans ??? tA st2' ? tB); //;
     554    nelim A; /2/; *; //;
     555##] nqed.
     556
     557(*
    527558Lemma simulation_star_forever_silent:
    528559  forall st1 st2,
Note: See TracChangeset for help on using the changeset viewer.