source: C-semantics/SmallstepExec.ma @ 24

Last change on this file since 24 was 24, checked in by campbell, 10 years ago

Separate out IOMonad from the rest of the executable semantics.
Start adding simulation results.

File size: 1.4 KB
RevLine 
[24]1
2include "extralib.ma".
3include "IOMonad.ma".
4include "Integers.ma".
5include "Events.ma".
6
7nrecord execstep : Type[1] ≝
8{ genv  : Type
9; state : Type
10; io : interaction
11; initial : state → Prop
12; final : state → int → Prop
13; step : genv → state → IO io (trace×state)
14}.
15
16nlet rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
17 : IO (io exec) (trace × (state exec)) ≝
18match n with
19[ O ⇒ Value ?? 〈E0, s〉
20| S n' ⇒ ! 〈t1,s1〉 ← step exec g s;:
21         repeat n' exec g s1
22].
23
24alias symbol "and" (instance 2) = "logical and".
25nrecord related_semantics : Type[1] ≝
26{ sem1 : execstep
27; sem2 : execstep
28; ge1 : genv sem1
29; ge2 : genv sem2
30; match_states : state sem1 → state sem2 → Prop
31; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
32; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r
33}.
34
35
36
37nrecord simulation : Type[1] ≝
38{ sems :> related_semantics
39; sim : ∀st1,st2,t,st1'.
40        P_io' (io (sem1 sems)) (trace × (state (sem1 sems))) (λr. r = 〈t,st1'〉) (step (sem1 sems) (ge1 sems) st1) →
41        match_states sems st1 st2 →
42        ∃st2':(state (sem2 sems)).(∃n:nat.P_io' (io (sem2 sems)) (trace × (state (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n (sem2 sems) (ge2 sems) st2)) ∧
43          match_states sems st1' st2'
44}.
Note: See TracBrowser for help on using the repository browser.