Changeset 3501


Ignore:
Timestamp:
Sep 25, 2014, 7:15:35 PM (5 years ago)
Author:
sacerdot
Message:

Final static_dynamic statement committed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3500 r3501  
    932932coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?.
    933933
    934 lemma static_dynamic :
     934lemma static_dynamic_inv :
    935935(* Given an assembly program *)
    936936∀p,p',prog.
    937937
    938 (* Given a Galois connection to an abstract transition system *)
     938(* Given an abstraction interpretation framework for the program *)
    939939∀R: asm_abstract_interpretation p p' prog.
    940940
     
    946946 terminated_trace … t → pre_measurable_trace … t →
    947947
    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) *)
    949949let labels ≝ chop … (get_costlabels_of_trace …  t) in
    950950
     
    11011101]
    11021102qed.
     1103
     1104definition 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
     1111theorem 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) *)
     1127let 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. *)
     1140R stn (〚abs_actions〛 a1).
Note: See TracChangeset for help on using the changeset viewer.