Changeset 2315


Ignore:
Timestamp:
Aug 31, 2012, 4:52:05 PM (7 years ago)
Author:
campbell
Message:

Add some more commentary.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2314 r2315  
    33include "utilities/bool.ma".
    44include "utilities/listb.ma".
     5include "RTLabs/CostMisc.ma".
    56
    67definition check_well_cost_fn : internal_function → bool ≝
     
    118119    check_label_bounded_spec g l tl toch toch.
    119120
    120 (* TODO: move (or is it somewhere already?) *)
    121121
    122122lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
     
    255255qed.
    256256
     257(* Show that when we remove labels from to_check we do actually find a bound
     258   (if it exists).  We need two extra facts: everything is "well" labelled,
     259   so that we know that branches are followed by labels and we don't need to
     260   follow them; and anything in the graph that isn't mentioned has already been
     261   successfully checked. *)
    257262
    258263lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'.
     
    328333] qed.
    329334
    330 include "RTLabs/CostMisc.ma".
     335
     336(* When we reject a label it is because we found a loop without a cost label
     337   when we followed its successors.  We need the invariant that only the
     338   initial label can be a cost label, and have two cases in the result: either
     339   we found the entire loop and return that, or we haven't come back out of the
     340   recursive calls to find the head again, so return part of the loop. *)
    331341
    332342lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM.
     
    390400     
    391401
    392 
     402(* Now keep checking as long as there's some instruction we haven't checked. *)
    393403
    394404let rec check_graph_bounded
     
    485495] qed.
    486496
     497(* The check_label_bounded_bad result gives us the loop, so we can use the
     498   loop_soundness_contradiction result to show that there's no bound for the
     499   head of the loop. *)
     500
    487501lemma check_graph_bounded_bad : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
    488502  check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = false →
Note: See TracChangeset for help on using the changeset viewer.