Ignore:
Timestamp:
Aug 16, 2012, 6:03:21 PM (8 years ago)
Author:
campbell
Message:

Nicer form of steps until cost label bound in RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostSpec.ma

    r2294 r2297  
    5959].
    6060
    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. *)
    6363
    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.
     64inductive bound_on_instrs_to_cost (g:graph statement) : label → nat → Prop ≝
     65| boitc_step : ∀l,n,H.
    7466    let stmt ≝ lookup_present … g l H in
    7567    (∀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)
     70with 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.
    7878
    7979definition 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.
    8181
    8282definition well_cost_labelled_program : RTLabs_program → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.