Changeset 1544 for src/common


Ignore:
Timestamp:
Nov 23, 2011, 6:01:15 PM (8 years ago)
Author:
sacerdot
Message:

StructuredTraces? inhabited for object code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1536 r1544  
    44inductive status_class : Type[0] ≝
    55| cl_return : status_class
     6| cl_jump   : status_class
    67| cl_call   : status_class
    7 | cl_cost   : status_class
    8 | cl_nocost : status_class
     8| cl_other : status_class
    99.
    1010
     
    1313  as_execute : as_status → as_status → Prop;
    1414  as_classifier : as_status → status_class → Prop;
     15  as_costed : as_status → Prop;
    1516  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    1617}.
     
    3940      ∀end_status: S.
    4041        trace_any_label S ends_flag start_status end_status →
    41         as_classifier S start_status cl_cost
     42        as_costed S start_status
    4243          trace_label_label S ends_flag start_status end_status
    4344with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
     
    4748        as_execute S start_status final_status →
    4849        ¬ as_classifier S start_status cl_return →
    49         as_classifier S final_status cl_cost
     50        as_costed S final_status
    5051          trace_any_label S doesnt_end_with_ret start_status final_status
    5152  | tal_base_return:
     
    5859      ∀end_flag: trace_ends_with_ret.
    5960      ∀status_pre_fun_call: S.
     61      ∀status_start_fun_call: S.
    6062      ∀status_after_fun_call: S.
    6163      ∀status_final: S.
    62       ∀status_start_fun_call: S.
    6364        as_execute S status_pre_fun_call status_start_fun_call →
    6465        ∀H:as_classifier S status_pre_fun_call cl_call.
     
    7071      ∀end_flag: trace_ends_with_ret.
    7172      ∀status_pre: S.
     73      ∀status_init: S.
    7274      ∀status_end: S.
    73       ∀status_init: S.
    7475        as_execute S status_pre status_init →
    7576        trace_any_label S end_flag status_init status_end →
    76         as_classifier S status_pre cl_nocost →
     77        as_classifier S status_pre cl_other →
     78        ¬ (as_costed S status_pre) →
    7779          trace_any_label S end_flag status_pre status_end.
    7880
     
    101103      ∀end_status: S.
    102104        trace_any_call S start_status end_status →
    103         as_classifier S start_status cl_cost
     105        as_costed S start_status
    104106        trace_label_call S start_status end_status
    105107       
     
    126128        as_execute S status_pre status_init →
    127129        trace_any_call S status_init status_end →
    128         as_classifier S status_pre cl_nocost →
     130        as_classifier S status_pre cl_other →
     131        ¬ (as_costed S status_pre) →
    129132          trace_any_call S status_pre status_end.
    130 
Note: See TracChangeset for help on using the changeset viewer.