Changeset 2596 for src/common


Ignore:
Timestamp:
Jan 31, 2013, 12:06:58 PM (7 years ago)
Author:
campbell
Message:

Use a simpler stack cost map, and then specialise to each semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2534 r2596  
    8686  pcs_exec :> fullexec io_out io_in;
    8787  pcs_labelled : ∀g. state … pcs_exec g → bool;
    88   pcs_classify : ∀g. state … pcs_exec g → status_class
     88  pcs_classify : ∀g. state … pcs_exec g → status_class;
     89  pcs_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
    8990}.
    9091
     
    9697definition measurable : ∀C:preclassified_system.
    9798  ∀p:program ?? C. nat → nat →
    98   (∀s. match pcs_classify … (make_global … p) s with  [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat) →
     99  (ident → nat) (* stack cost *) →
    99100  nat → Prop ≝
    100101λC,p,m,n,stack_cost,max_allowed_stack.  ∃prefix,suffix,interesting,remainder.
    101   let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) stack_cost in
     102  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?) in
    102103  let cl_trace ≝ exec_inf … (cs_exec … C') p in
    103104  split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
Note: See TracChangeset for help on using the changeset viewer.