source: C-semantics/SmallstepExec.ma @ 24

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

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

File size: 1.4 KB
Line 
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.