Changeset 2928


Ignore:
Timestamp:
Mar 21, 2013, 6:26:46 PM (4 years ago)
Author:
tranquil
Message:

some sketches about correctness proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2875 r2928  
    114114   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    115115
     116include "common/ExtraMonads.ma".
     117
    116118theorem correct' :
    117119  ∀observe.
     
    124126  ∧
    125127  simulates output.
     128#observe #p_in #out
     129#H @('bind_inversion H) -H
     130** #init_cost #labelled #p_rtlabs #EQ_front_end
     131#H @('bind_inversion H) -H
     132** #p_asm #stack_costs #globals_size
     133#H @('bind_inversion H) -H
     134#p_asm'
     135#H lapply (opt_eq_from_res ???? H) #EQ_lin_to_asm
     136whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
     137#H @('bind_inversion H) -H
     138#p_loc #EQ_assembler
     139whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
     140#NOT_WRONG %
     141[ cases daemon (* TODO *)
     142| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
     143
     144cut (∀n,s1,s2,obs1,obs2.
     145          exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 →
     146            ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2.
     147            tlr_observables … tlr (function_of … s1) = obs2 →
     148            (* maybe instead of function_of the called id can rather be obtained from execution? *)
     149     ∃m,p,s_fin.
     150   observables (OC_preclassified_system (c_labelled_object_code … p))
     151    (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
     152   
     153     
     154             
     155             
    126156 
    127157(* start of old simulates 
Note: See TracChangeset for help on using the changeset viewer.