Changeset 2852


Ignore:
Timestamp:
Mar 12, 2013, 4:37:30 PM (4 years ago)
Author:
mckinna
Message:

Interim commit to re-establish well-typedness after all the recent changes to compiler.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2802 r2852  
    77
    88theorem correct :
    9   ∀input_program,output.
     9  ∀observe,input_program,output.
    1010(*  ∀lobject_code,labelled,cost_map. *)
    11   compile input_program = OK ? output →
     11  compile observe input_program = return output →
    1212
    1313  not_wrong … (exec_inf … clight_fullexec input_program) →
     
    1919  True (* TODO *).
    2020
    21 #input_program #output
     21#observe #input_program #output
    2222#COMPILE
    2323#NOT_WRONG
     
    114114
    115115theorem correct' :
     116  ∀observe.
    116117  ∀input_program,output.
    117   ∀initial_status.
    118   compile input_program = OK ? output →
     118  compile observe input_program = return output →
    119119  not_wrong … (exec_inf … clight_fullexec input_program) →
    120120  sim_with_labels
Note: See TracChangeset for help on using the changeset viewer.