Changeset 1730 for src/ERTL/liveness.ma


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

Minor changes while studying the proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.