Changeset 2297 for src/RTLabs/CostSpec.ma

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:

• src/RTLabs/CostSpec.ma (modified) (1 diff)

src/RTLabs/CostSpec.ma

@@ -59 +59 @@
 ].
 
-definition steps_for_statement : statement → nat ≝
-λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
+(* To show that the labelling is sound we need a bound on the number of
+   instructions in the current function until the next cost label. *)
 
-inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
-| bostc_here : ∀l,n,H.
-    is_cost_label (lookup_present … g l H) →
-    bound_on_steps_to_cost g l n
-| bostc_later : ∀l,n,H.
-    ¬ is_cost_label (lookup_present … g l H) →
-    bound_on_steps_to_cost1 g l n →
-    bound_on_steps_to_cost g l n
-with bound_on_steps_to_cost1 : label → nat → Prop ≝
-| bostc_step : ∀l,n,H.
+inductive bound_on_instrs_to_cost (g:graph statement) : label → nat → Prop ≝
+| boitc_step : ∀l,n,H.
     let stmt ≝ lookup_present … g l H in
     (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
-          bound_on_steps_to_cost g l' n) →
-    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
+          bound_on_instrs_to_cost' g l' n) →
+    bound_on_instrs_to_cost g l (S n)
+with bound_on_instrs_to_cost' : label → nat → Prop ≝
+| boitc_here : ∀l,n,H.
+    is_cost_label (lookup_present … g l H) →
+    bound_on_instrs_to_cost' g l n
+| boitc_later : ∀l,n,H.
+    ¬ is_cost_label (lookup_present … g l H) →
+    bound_on_instrs_to_cost g l n →
+    bound_on_instrs_to_cost' g l n.
 
 definition soundly_labelled_fn : internal_function → Prop ≝
-λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
+λf. ∀l. present … (f_graph f) l → ∃n. bound_on_instrs_to_cost (f_graph f) l n.
 
 definition well_cost_labelled_program : RTLabs_program → Prop ≝