Changeset 3096 for src/ASM


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

preliminary work on closing correctness.ma

Location:
src/ASM
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r3065 r3096  
    157157   (λst. return (execute_1_pseudo_instruction' … addr_of_label addr_of_symbol sigma policy st))
    158158   (initialise_status … c).
     159
     160definition ASM_status:
     161 ∀prog:pseudo_assembly_program.
     162 ∀sigma,policy.abstract_status ≝
     163  λc,sigma,policy.
     164  let label_map ≝ \fst (create_label_cost_map (code … c)) in
     165  let symbol_map ≝ construct_datalabels (preamble … c) in
     166  let addr_of_label ≝ λx.bitvector_of_nat ? (lookup_def … label_map x 0) in
     167  let addr_of_symbol ≝ λx.lookup_def … symbol_map x (addr_of_label x) in
     168  ASM_abstract_status c addr_of_label addr_of_symbol sigma policy.
     169
Note: See TracChangeset for help on using the changeset viewer.