Changeset 3509
 Timestamp:
 Sep 26, 2014, 6:12:07 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Final.ma
r3507 r3509 37 37 ∃s1',s2'. measurable … s1' s2' … t'. 38 38 39 axiom cerco:39 theorem cerco: 40 40 (* Given the operational semantics of a source program *) 41 41 ∀S1: abstract_status. … … 68 68 (* There exists a corresponding target trace starting from si' *) 69 69 ∃sn'. ∃t': raw_trace … si' sn'. 70 Srel … sn sn' ∧71 get_costlabels_of_trace … t = get_costlabels_of_trace … t' ∧70 Srel … rel sn sn' ∧ 71 ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'. 72 72 73 73 (* that has a measurable fragment starting in s1' and ending in s2' *) … … 90 90 obtained by applying every semantics in abs_trace. *) 91 91 R s2' (〚abs_actions〛 a1). 92 [2: @hide_prf 92 [2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf 93 93 cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) * 94 94 #lbl' #pc * #Hmem #EQ destruct … … 96 96 @(proj2 … (static_analisys_ok … EQmap … Hmem)) 97 97 ] 98 cases daemon 99 qed.
Note: See TracChangeset
for help on using the changeset viewer.