Changeset 1730 for src/ERTL

Timestamp:

Feb 23, 2012, 5:17:32 PM (8 years ago)

Author:

sacerdot

Message:

Minor changes while studying the proof.

Location:

src/ERTL

Files:

• Interference.ma (modified) (1 diff)
• liveness.ma (modified) (4 diffs)

src/ERTL/Interference.ma

@@ -27 +27 @@
 ; prop_colouring: ∀l. ∀v1, v2: vertex.
    is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
-; prop_colouring2:
+; prop_colouring2: (*CSC: the exist-guarded premise is just to make the proof more general *)
    ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no
+(* CSC: useless for the proof and very weak
 ; prop_colouring3:
    spilled_no = 0 ∨
     ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1)
+*)
 }.
 

src/ERTL/liveness.ma

@@ -278 +278 @@
   λglobals: list ident.
   λint_fun: ertl_internal_function globals.
-  λlivebefore: label → ?.
   λlabel.
   λliveafter: valuation.
@@ -284 +283 @@
   [ None      ⇒ ?
   | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
-      lattice_join (livebefore successor liveafter) accu)
+      lattice_join (livebefore globals int_fun successor liveafter) accu)
       (statement_successors globals stmt) lattice_bottom
   ].
@@ -300 +299 @@
     ∀globals: list ident.
     ∀int_fun.
-    let f ≝ liveafter globals int_fun (livebefore globals int_fun) in
+    ∀f. (* CSC: was let f ≝ liveafter globals int_fun in *)
       ∀v: label.
-        lattice_equal (f v (fix_lfp f)) (fix_lfp f v)
+        lattice_equal (f v (fix_lfp f)) (fix_lfp f v) (*CSC: TOO STRONG: WE ONLY NEED CORRECTNESS NOT COMPLETENESS *)
 }.
 
@@ -310 +309 @@
   λglobals.
   λint_fun.
-    the_fixpoint (liveafter globals int_fun (livebefore globals int_fun)).
+    the_fixpoint (liveafter globals int_fun).