- Timestamp:
- Feb 23, 2012, 5:17:32 PM (9 years ago)
- Location:
- src/ERTL
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/Interference.ma
r1429 r1730 27 27 ; prop_colouring: ∀l. ∀v1, v2: vertex. 28 28 is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 29 ; prop_colouring2: 29 ; prop_colouring2: (*CSC: the exist-guarded premise is just to make the proof more general *) 30 30 ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no 31 (* CSC: useless for the proof and very weak 31 32 ; prop_colouring3: 32 33 spilled_no = 0 ∨ 33 34 ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1) 35 *) 34 36 }. 35 37 -
src/ERTL/liveness.ma
r1729 r1730 278 278 λglobals: list ident. 279 279 λint_fun: ertl_internal_function globals. 280 λlivebefore: label → ?.281 280 λlabel. 282 281 λliveafter: valuation. … … 284 283 [ None ⇒ ? 285 284 | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice. 286 lattice_join (livebefore successor liveafter) accu)285 lattice_join (livebefore globals int_fun successor liveafter) accu) 287 286 (statement_successors globals stmt) lattice_bottom 288 287 ]. … … 300 299 ∀globals: list ident. 301 300 ∀int_fun. 302 let f ≝ liveafter globals int_fun (livebefore globals int_fun) in301 ∀f. (* CSC: was let f ≝ liveafter globals int_fun in *) 303 302 ∀v: label. 304 lattice_equal (f v (fix_lfp f)) (fix_lfp f v) 303 lattice_equal (f v (fix_lfp f)) (fix_lfp f v) (*CSC: TOO STRONG: WE ONLY NEED CORRECTNESS NOT COMPLETENESS *) 305 304 }. 306 305 … … 310 309 λglobals. 311 310 λint_fun. 312 the_fixpoint (liveafter globals int_fun (livebefore globals int_fun)).311 the_fixpoint (liveafter globals int_fun).
Note: See TracChangeset
for help on using the changeset viewer.