Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3500 r3501 932 932 coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?. 933 933 934 lemma static_dynamic :934 lemma static_dynamic_inv : 935 935 (* Given an assembly program *) 936 936 ∀p,p',prog. 937 937 938 (* Given a Galois connection to an abstract transition system *)938 (* Given an abstraction interpretation framework for the program *) 939 939 ∀R: asm_abstract_interpretation p p' prog. 940 940 … … 946 946 terminated_trace … t → pre_measurable_trace … t → 947 947 948 (* Let labels be the costlabels observed in the trace , excluding the last one*)948 (* Let labels be the costlabels observed in the trace (last one excluded) *) 949 949 let labels ≝ chop … (get_costlabels_of_trace … t) in 950 950 … … 1101 1101 ] 1102 1102 qed. 1103 1104 definition measurable : 1105 ∀S: abstract_status. ∀s1,s2,s4 : S. raw_trace … s1 s4 → Prop ≝ 1106 λS,s1,s2,s4,t. 1107 ∃s3:S. ∃t' : raw_trace … s2 s3. ∃l1,l2,prf1,prf2. 1108 t = t_ind ? s1 s2 s4 l1 prf1 … (t' @ (t_ind ? s3 s4 s4 l2 prf2 … (t_base … s4))) 1109 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ pre_measurable_trace … t. 1110 1111 theorem static_dynamic : 1112 (* Given an assembly program *) 1113 ∀p,p',prog. 1114 1115 (* Given an abstraction interpretation framework for the program *) 1116 ∀R: asm_abstract_interpretation p p' prog. 1117 1118 (* If the static analysis does not fail *) 1119 ∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1. 1120 1121 (* For every measurable trace whose second state is st1 or, equivalently, 1122 whose first state after the initial labelled transition is st1 *) 1123 ∀st0,st1,stn. ∀t: raw_trace (asm_operational_semantics … prog) … st0 stn. 1124 measurable … st1 … t → 1125 1126 (* Let labels be the costlabels observed in the trace (last one excluded) *) 1127 let labels ≝ chop … (get_costlabels_of_trace … t) in 1128 1129 (* Let abs_actions be the list of statically computed abstract actions 1130 associated to each label in labels. *) 1131 ∀abs_actions. 1132 abs_actions = 1133 dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) → 1134 1135 (* Given an abstract state in relation with the second state of the trace *) 1136 ∀a1.R st1 a1 → 1137 1138 (* The final state of the trace is in relation with the one obtained by 1139 applying every semantics in abs_trace. *) 1140 R stn (〚abs_actions〛 a1).
Note: See TracChangeset
for help on using the changeset viewer.