Changeset 2315
 Timestamp:
 Aug 31, 2012, 4:52:05 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostCheck.ma
r2314 r2315 3 3 include "utilities/bool.ma". 4 4 include "utilities/listb.ma". 5 include "RTLabs/CostMisc.ma". 5 6 6 7 definition check_well_cost_fn : internal_function → bool ≝ … … 118 119 check_label_bounded_spec g l tl toch toch. 119 120 120 (* TODO: move (or is it somewhere already?) *)121 121 122 122 lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'. … … 255 255 qed. 256 256 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. *) 257 262 258 263 lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'. … … 328 333 ] qed. 329 334 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. *) 331 341 332 342 lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM. … … 390 400 391 401 392 402 (* Now keep checking as long as there's some instruction we haven't checked. *) 393 403 394 404 let rec check_graph_bounded … … 485 495 ] qed. 486 496 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 487 501 lemma check_graph_bounded_bad : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM. 488 502 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.