Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 years ago)
Author:
tranquil
Message:

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File:
1 moved

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLINAxiom.ma

    r2868 r2946  
    88axiom LTLToLIN_ok :
    99∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
    10 ∀p_in : LTL_program.
     10∀p_in : joint_program LTL.
    1111let p_out ≝ ltl_to_lin p_in in
    1212∃[1] R.
     
    1414    (joint_status LTL_semantics p_in stacksizes)
    1515    (joint_status LIN_semantics p_out stacksizes)
    16     R.
     16    R ∧
     17  ∀init_in.make_initial_state
     18    (mk_prog_params LTL_semantics p_in stacksizes) = OK … init_in →
     19  ∃init_out.
     20    make_initial_state
     21     (mk_prog_params LIN_semantics p_out stacksizes) =
     22      OK ? init_out ∧
     23   R init_in init_out.
Note: See TracChangeset for help on using the changeset viewer.