Changeset 2852

Timestamp:

Mar 12, 2013, 4:37:30 PM (7 years ago)

Author:

mckinna

Message:

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

File:

• src/correctness.ma (modified) (3 diffs)

src/correctness.ma

@@ -7 +7 @@
 
 theorem correct :
-  ∀input_program,output.
+  ∀observe,input_program,output.
 (*  ∀lobject_code,labelled,cost_map. *)
-  compile input_program = OK ? output →
+  compile observe input_program = return output →
 
   not_wrong … (exec_inf … clight_fullexec input_program) →
@@ -19 +19 @@
   True (* TODO *).
 
-#input_program #output
+#observe #input_program #output
 #COMPILE
 #NOT_WRONG
@@ -114 +114 @@
 
 theorem correct' :
+  ∀observe.
   ∀input_program,output.
-  ∀initial_status.
-  compile input_program = OK ? output →
+  compile observe input_program = return output →
   not_wrong … (exec_inf … clight_fullexec input_program) →
   sim_with_labels