Changeset 1996


Ignore:
Timestamp:
May 25, 2012, 9:18:04 AM (5 years ago)
Author:
campbell
Message:

Work on correctness from yesterday.

Location:
src
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r1606 r1996  
    1717 λp. ticks_of … (mk_policy p).
    1818
     19(*
    1920definition execute_1_pseudo_instruction_trace:
    2021 (Word → nat × nat) → PseudoStatus → IO io_out io_in (trace × PseudoStatus) ≝
     
    5758definition ASM_fullexec: fullexec io_out io_in ≝
    5859 mk_fullexec … exec make_global (λp.OK … (load (\fst p) (initialise_status … (Stub ??)))).
     60*)
     61axiom ASM_fullexec: fullexec io_out io_in.
Note: See TracChangeset for help on using the changeset viewer.