Changeset 2946 for src/LTL/LTLToLINAxiom.ma

Timestamp:

Mar 24, 2013, 11:29:01 AM (8 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:

• src/LTL/LTLToLINAxiom.ma (moved) (moved from src/LTL/LTLToLINProof.ma) (2 diffs)

src/LTL/LTLToLINAxiom.ma

@@ -8 +8 @@
 axiom LTLToLIN_ok :
 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
-∀p_in : LTL_program.
+∀p_in : joint_program LTL.
 let p_out ≝ ltl_to_lin p_in in
 ∃[1] R.
@@ -14 +14 @@
     (joint_status LTL_semantics p_in stacksizes)
     (joint_status LIN_semantics p_out stacksizes)
-    R.
+    R ∧
+  ∀init_in.make_initial_state
+    (mk_prog_params LTL_semantics p_in stacksizes) = OK … init_in →
+  ∃init_out.
+    make_initial_state
+     (mk_prog_params LIN_semantics p_out stacksizes) =
+      OK ? init_out ∧
+   R init_in init_out.