Ignore:
Timestamp:
Apr 5, 2013, 6:04:14 PM (7 years ago)
Author:
tranquil
Message:

preliminary work on closing correctness.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASMAxiom.ma

    r2946 r3096  
    1717include "joint/Traces.ma".
    1818include "common/StatusSimulation.ma".
    19 
    20 (* atm ASM_abstract_status is related to object code, not ASM... *)
    21 axiom ASM_status : pseudo_assembly_program → abstract_status.
    22 axiom make_ASM_initial_state : ∀p.res (ASM_status p).
     19include "ASM/Interpret2.ma".
    2320
    2421axiom LINToASM_ok :
     
    2623∀p_in : joint_program LIN.
    2724∀p_out : pseudo_assembly_program.
     25∀sigma,policy.
    2826lin_to_asm p_in = Some ? p_out →
     27∀init_in.make_initial_state
     28    (mk_prog_params LIN_semantics p_in stacksizes) = OK … init_in →
     29let init_out ≝ initialise_status … p_out in
    2930∃[1] R.
    30   status_simulation
     31  status_simulation_with_init
    3132    (joint_status LIN_semantics p_in stacksizes)
    32     (ASM_status p_out)
    33     R ∧
    34   ∀init_in.make_initial_state
    35     (mk_prog_params LIN_semantics p_in stacksizes) = OK … init_in →
    36   ∃init_out.
    37     make_ASM_initial_state p_out =
    38       OK ? init_out ∧
    39    R init_in init_out.
     33    (ASM_status p_out sigma policy)
     34    R init_in init_out.
Note: See TracChangeset for help on using the changeset viewer.