Changeset 2297 for src/RTLabs/CostSpec.ma
 Timestamp:
 Aug 16, 2012, 6:03:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostSpec.ma
r2294 r2297 59 59 ]. 60 60 61 definition steps_for_statement : statement → nat ≝ 62 λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1  St_call_ptr _ _ _ _ ⇒ 1  St_return ⇒ 1  _ ⇒ 0 ]). 61 (* To show that the labelling is sound we need a bound on the number of 62 instructions in the current function until the next cost label. *) 63 63 64 inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝ 65  bostc_here : ∀l,n,H. 66 is_cost_label (lookup_present … g l H) → 67 bound_on_steps_to_cost g l n 68  bostc_later : ∀l,n,H. 69 ¬ is_cost_label (lookup_present … g l H) → 70 bound_on_steps_to_cost1 g l n → 71 bound_on_steps_to_cost g l n 72 with bound_on_steps_to_cost1 : label → nat → Prop ≝ 73  bostc_step : ∀l,n,H. 64 inductive bound_on_instrs_to_cost (g:graph statement) : label → nat → Prop ≝ 65  boitc_step : ∀l,n,H. 74 66 let stmt ≝ lookup_present … g l H in 75 67 (∀l'. Exists label (λl0. l0 = l') (successors stmt) → 76 bound_on_steps_to_cost g l' n) → 77 bound_on_steps_to_cost1 g l (steps_for_statement stmt + n). 68 bound_on_instrs_to_cost' g l' n) → 69 bound_on_instrs_to_cost g l (S n) 70 with bound_on_instrs_to_cost' : label → nat → Prop ≝ 71  boitc_here : ∀l,n,H. 72 is_cost_label (lookup_present … g l H) → 73 bound_on_instrs_to_cost' g l n 74  boitc_later : ∀l,n,H. 75 ¬ is_cost_label (lookup_present … g l H) → 76 bound_on_instrs_to_cost g l n → 77 bound_on_instrs_to_cost' g l n. 78 78 79 79 definition soundly_labelled_fn : internal_function → Prop ≝ 80 λf. ∀l. present … (f_graph f) l → ∃n. bound_on_ steps_to_cost1(f_graph f) l n.80 λf. ∀l. present … (f_graph f) l → ∃n. bound_on_instrs_to_cost (f_graph f) l n. 81 81 82 82 definition well_cost_labelled_program : RTLabs_program → Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.