Changeset 2800 for src


Ignore:
Timestamp:
Mar 7, 2013, 1:07:31 PM (7 years ago)
Author:
campbell
Message:

Tidy up Measurable.ma a little, get rid of obsolete comments.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2795 r2800  
    2424definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝
    2525λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
     26
     27(* Construction of the trace of intensional events.
     28
     29   It might be possible to merge these with the plain events, but for now we
     30   combine those with call/return information taken from the states.
     31   
     32   The build_* results help with the proof that measurable subtraces are
     33   preserved in the front-end. *)
    2634
    2735definition intensional_event_of_event : event → list intensional_event ≝
     
    7381%
    7482qed.
    75 
    76 lemma flatten_append : ∀A,l1,l2.
    77   flatten A (l1@l2) = (flatten A l1)@(flatten A l2).
    78 #A #l1 #l2
    79 elim l1
    80 [ %
    81 | #h #t #IH whd in ⊢ (??%(??%?));
    82   change with (flatten ??) in match (foldr ?????); >IH
    83   change with (flatten ??) in match (foldr ?????);
    84   >associative_append %
    85 ] qed.
    8683
    8784
     
    211208] qed.
    212209
     210(* I had a little trouble doing this directly. *)
    213211lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop.
    214212  (∀f. P f (f H)) →
     
    247245  #cs' #tl' >associative_append %
    248246] qed.
    249  
     247
     248(* Measuring stack usage.  TODO: I think there's another version of this from
     249   the back-end that should be merged. *) 
    250250
    251251definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝
     
    366366  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?).
    367367
    368 (* FIXME: this definition is unreasonable because it presumes we can easily
    369    identify the change in stack usage from return states, but that information
    370    is rather implicit (we only really record the function called in the
    371    extended RTLabs states when building the structured traces). *)
     368
    372369
    373370definition measurable : ∀C:preclassified_system.
     
    385382  le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack.
    386383
    387 (* TODO: probably ought to be elsewhere; use exec_steps instead
    388 
    389    Note that this does not include stack space
    390  *)
     384
    391385
    392386definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝
  • src/utilities/lists.ma

    r2443 r2800  
    244244]
    245245qed.
     246
     247
     248
     249lemma flatten_append : ∀A,l1,l2.
     250  flatten A (l1@l2) = (flatten A l1)@(flatten A l2).
     251#A #l1 #l2
     252elim l1
     253[ %
     254| #h #t #IH whd in ⊢ (??%(??%?));
     255  change with (flatten ??) in match (foldr ?????); >IH
     256  change with (flatten ??) in match (foldr ?????);
     257  >associative_append %
     258] qed.
    246259
    247260
     
    352365
    353366
    354 (* Not terribly efficient sort for testing purposes *)
     367(* A not terribly efficient sort for testing purposes *)
    355368
    356369let rec ordered_insert (A:Type[0]) (lt:A → A → bool) (a:A) (l:list A) on l : list A ≝
Note: See TracChangeset for help on using the changeset viewer.