Changeset 2202 for src/Clight/labelSpecification.ma
- Timestamp:
- Jul 17, 2012, 6:57:39 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/labelSpecification.ma
r2201 r2202 1 1 include "Clight/Cexec.ma". 2 2 include "Clight/label.ma". 3 include "common/Executions.ma". 3 4 4 5 (* Formalise the notion of a trace with extra cost labels added. Note that … … 9 10 | twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2). 10 11 11 (* A finite trace is produced by some prefix of an execution. *)12 13 inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝14 | steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)15 | steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e16 | steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.17 18 12 (* One execution is simulated by another, but possibly using more steps and 19 13 introducing some cost labels. *) … … 21 15 coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝ 22 16 | swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2. 23 steps tr2 e2 (e_stop … tr2' r s2) →17 steps state tr2 e2 (e_stop … tr2' r s2) → 24 18 trace_with_extra_labels tr1 tr2 → 25 19 sim_with_labels (e_stop … tr1 r s1) e2 26 20 | swl_steps : ∀tr1,tr2,s1,e1,e2,e2'. 27 steps tr2 e2 e2' →21 steps state tr2 e2 e2' → 28 22 trace_with_extra_labels tr1 tr2 → 29 23 sim_with_labels e1 e2' → … … 33 27 sim_with_labels (e_interact … o k1) (e_interact … o k2). 34 28 35 (* We do not consider wrong executions. *)36 37 coinductive not_wrong : execution state io_out io_in → Prop ≝38 | nw_stop : ∀tr,i,s. not_wrong (e_stop … tr i s)39 | nw_step : ∀tr,s,e. not_wrong e → not_wrong (e_step … tr s e)40 | nw_interact : ∀o,k. (∀i. not_wrong (k i)) → not_wrong (e_interact … o k).41 42 29 (* Desired result *) 43 30 … … 46 33 let e1 ≝ exec_inf … clight_fullexec p in 47 34 let e2 ≝ exec_inf … clight_fullexec (clight_label p) in 48 not_wrong e1 →35 not_wrong state e1 → 49 36 sim_with_labels e1 e2.
Note: See TracChangeset
for help on using the changeset viewer.