Ignore:
Timestamp:
Mar 8, 2012, 12:13:11 PM (8 years ago)
Author:
campbell
Message:

Provide a combined type for terminating and non-terminating structured
traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1808 r1812  
    167167            trace_label_diverges_exists S status_initial.
    168168
     169
     170inductive trace_whole_program (S:abstract_status) : S → Type[0] ≝
     171  | twp_terminating:
     172      ∀status_initial: S.
     173      ∀status_start_fun: S.
     174      ∀status_final: S.
     175        as_classifier S status_initial cl_call →
     176        as_execute S status_initial status_start_fun →
     177        trace_label_return S status_start_fun status_final →
     178        trace_whole_program S status_initial
     179  | twp_diverges:
     180      ∀status_initial: S.
     181      ∀status_start_fun: S.
     182        as_classifier S status_initial cl_call →
     183        as_execute S status_initial status_start_fun →
     184        trace_label_diverges S status_start_fun →
     185        trace_whole_program S status_initial.
     186
     187(* Again, an identical version in Prop for existence proofs. *)
     188inductive trace_whole_program_exists (S:abstract_status) : S → Prop ≝
     189  | twp_terminating:
     190      ∀status_initial: S.
     191      ∀status_start_fun: S.
     192      ∀status_final: S.
     193        as_classifier S status_initial cl_call →
     194        as_execute S status_initial status_start_fun →
     195        trace_label_return S status_start_fun status_final →
     196        trace_whole_program_exists S status_initial
     197  | twp_diverges:
     198      ∀status_initial: S.
     199      ∀status_start_fun: S.
     200        as_classifier S status_initial cl_call →
     201        as_execute S status_initial status_start_fun →
     202        trace_label_diverges_exists S status_start_fun →
     203        trace_whole_program_exists S status_initial.
     204
     205
    169206let rec trace_any_label_label S s s' f
    170207  (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
Note: See TracChangeset for help on using the changeset viewer.