Changeset 1927 for src/common


Ignore:
Timestamp:
May 9, 2012, 1:05:21 PM (8 years ago)
Author:
mulligan
Message:

Reduced complexity of good_program predicate, ported to new notion of as_label, reintroduced some deleted code from common/StructuredTraces.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1926 r1927  
    1414
    1515record abstract_status : Type[1] ≝
    16   { as_status :> Type[0]
     16{
     17    as_status :> Type[0]
    1718  ; as_execute : as_status → as_status → Prop
    1819  ; as_pc : DeqSet
     
    122123 ].
    123124
     125definition as_trace_any_label_length':
     126    ∀S: abstract_status.
     127    ∀trace_ends_flag: trace_ends_with_ret.
     128    ∀start_status: S.
     129    ∀final_status: S.
     130    ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
     131      nat ≝
     132  λS: abstract_status.
     133  λtrace_ends_flag: trace_ends_with_ret.
     134  λstart_status: S.
     135  λfinal_status: S.
     136  λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
     137    |tal_pc_list … the_trace|.
     138
    124139let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
    125140  match tlr with
     
    140155    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    141156    tal_unrepeating … tl
     157  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
    142158  | _ ⇒ True
    143159  ].
     
    204220  λS,st1,st2,tr.match tr with
    205221  [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf»
    206   ].       
    207 
     222  ].
     223   
    208224coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
    209225  | tld_step:
Note: See TracChangeset for help on using the changeset viewer.