source: Deliverables/D3.1/C-semantics/SmallstepExec.ma @ 535

Last change on this file since 535 was 469, checked in by campbell, 8 years ago

Update work-in-progress file to match current development.

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