source: src/common/StructuredTraces.ma @ 1531

Last change on this file since 1531 was 1531, checked in by campbell, 8 years ago

A notion of abstract structured traces.

File size: 5.5 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3
4inductive status_class : Type[0] ≝
5| cl_return : status_class
6| cl_jump   : status_class
7| cl_call   : status_class
8| cl_cost   : status_class
9| cl_nocost : status_class
10.
11
12record abstract_status : Type[1] ≝ {
13  as_status :> Type[0];
14  as_execute : as_status → as_status → Prop;
15  as_classifier : as_status → status_class;
16  as_after_return : (Σs:as_status. as_classifier s = cl_call) → as_status → bool
17}.
18
19inductive trace_ends_with_ret: Type[0] ≝
20  | ends_with_ret: trace_ends_with_ret
21  | doesnt_end_with_ret: trace_ends_with_ret.
22
23inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
24  | tlr_base:
25      ∀status_before: S.
26      ∀status_after: S.
27        trace_label_label S ends_with_ret status_before status_after →
28        trace_label_return S status_before status_after
29  | tlr_step:
30      ∀status_initial: S.
31      ∀status_labelled: S.
32      ∀status_final: S.
33        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
34        trace_label_return S status_labelled status_final →
35          trace_label_return S status_initial status_final
36with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
37  | tll_base:
38      ∀ends_flag: trace_ends_with_ret.
39      ∀start_status: S.
40      ∀end_status: S.
41        trace_any_label S ends_flag start_status end_status →
42        as_classifier S start_status = cl_cost →
43          trace_label_label S ends_flag start_status end_status
44with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
45  | tal_base_not_return:
46      ∀start_status: S.
47      ∀final_status: S.
48        as_execute S start_status final_status →
49        as_classifier S start_status ≠ cl_return →
50        as_classifier S final_status = cl_cost →
51          trace_any_label S doesnt_end_with_ret start_status final_status
52  | tal_base_jump_jump:
53      ∀start_status: S.
54      ∀mid_status: S.
55      ∀final_status: S.
56        as_execute S start_status mid_status →
57        as_execute S mid_status final_status →
58        as_classifier S start_status = cl_jump →
59        as_classifier S mid_status = cl_jump →
60        as_classifier S final_status = cl_cost →
61          trace_any_label S doesnt_end_with_ret start_status final_status
62  | tal_base_return:
63      ∀start_status: S.
64      ∀final_status: S.
65        as_execute S start_status final_status →
66        as_classifier S start_status = cl_return →
67          trace_any_label S ends_with_ret start_status final_status
68  | tal_step_call:
69      ∀end_flag: trace_ends_with_ret.
70      ∀status_pre_fun_call: S.
71      ∀status_after_fun_call: S.
72      ∀status_final: S.
73      ∀status_start_fun_call: S.
74        as_execute S status_pre_fun_call status_start_fun_call →
75        ∀H:as_classifier S status_pre_fun_call = cl_call.
76          as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call = true →
77          trace_label_return S status_start_fun_call status_after_fun_call →
78          trace_any_label S end_flag status_after_fun_call status_final →
79            trace_any_label S end_flag status_pre_fun_call status_final
80  | tal_step_default:
81      ∀end_flag: trace_ends_with_ret.
82      ∀status_pre: S.
83      ∀status_end: S.
84      ∀status_init: S.
85        as_execute S status_pre status_init →
86        trace_any_label S end_flag status_init status_end →
87        as_classifier S status_pre = cl_nocost →
88          trace_any_label S end_flag status_pre status_end.
89
90
91coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
92  | tld_step:
93      ∀status_initial: S.
94      ∀status_labelled: S.
95          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
96          trace_label_diverges S status_labelled →
97            trace_label_diverges S status_initial
98  | tld_base:
99      ∀status_initial: S.
100      ∀status_pre_fun_call: S.
101      ∀status_after_fun_call: S.
102      ∀status_start_fun_call: S.
103        trace_label_call S status_initial status_pre_fun_call →
104        as_execute S status_pre_fun_call status_start_fun_call →
105        ∀H:as_classifier S status_pre_fun_call = cl_call.
106          trace_label_diverges S status_start_fun_call →
107            trace_label_diverges S status_initial
108             
109with trace_label_call: S → S → Type[0] ≝
110  | tlc_base:
111      ∀start_status: S.
112      ∀end_status: S.
113        trace_any_call S start_status end_status →
114        as_classifier S start_status = cl_cost →
115        trace_label_call S start_status end_status
116       
117with trace_any_call: S → S → Type[0] ≝
118  | tac_base:
119      ∀status: S.
120        as_classifier S status = cl_call →
121          trace_any_call S status status
122  | tac_step_call:
123      ∀status_pre_fun_call: S.
124      ∀status_after_fun_call: S.
125      ∀status_final: S.
126      ∀status_start_fun_call: S.
127        as_execute S status_pre_fun_call status_start_fun_call →
128        ∀H:as_classifier S status_pre_fun_call = cl_call.
129          as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call = true →
130          trace_label_return S status_start_fun_call status_after_fun_call →
131          trace_any_call S status_after_fun_call status_final →
132            trace_any_call S status_pre_fun_call status_final
133  | tac_step_default:
134      ∀status_pre: S.
135      ∀status_end: S.
136      ∀status_init: S.
137        as_execute S status_pre status_init →
138        trace_any_call S status_init status_end →
139        as_classifier S status_pre = cl_nocost →
140          trace_any_call S status_pre status_end.
141
Note: See TracBrowser for help on using the repository browser.