Changeset 1730


Ignore:
Timestamp:
Feb 23, 2012, 5:17:32 PM (8 years ago)
Author:
sacerdot
Message:

Minor changes while studying the proof.

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Interference.ma

    r1429 r1730  
    2727; prop_colouring: ∀l. ∀v1, v2: vertex.
    2828   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 *)
    3030   ∀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
    3132; prop_colouring3:
    3233   spilled_no = 0 ∨
    3334    ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1)
     35*)
    3436}.
    3537
  • src/ERTL/liveness.ma

    r1729 r1730  
    278278  λglobals: list ident.
    279279  λint_fun: ertl_internal_function globals.
    280   λlivebefore: label → ?.
    281280  λlabel.
    282281  λliveafter: valuation.
     
    284283  [ None      ⇒ ?
    285284  | 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)
    287286      (statement_successors globals stmt) lattice_bottom
    288287  ].
     
    300299    ∀globals: list ident.
    301300    ∀int_fun.
    302     let f ≝ liveafter globals int_fun (livebefore globals int_fun) in
     301    ∀f. (* CSC: was let f ≝ liveafter globals int_fun in *)
    303302      ∀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 *)
    305304}.
    306305
     
    310309  λglobals.
    311310  λ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.