Changeset 3022 for src/RTLabs


Ignore:
Timestamp:
Mar 28, 2013, 7:49:22 PM (7 years ago)
Author:
campbell
Message:

Make a couple of tests monadic for easier inversion.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2728 r3022  
    626626] qed.
    627627
     628
     629definition check_cost_program_prf : ∀p:RTLabs_program. res (well_cost_labelled_program p) ≝
     630λp. (match check_cost_program p return λb. bool_to_Prop b ↔ well_cost_labelled_program p → res ? with
     631     [ true ⇒ λH. OK ??
     632     | false ⇒ λ_. Error ? (msg BadCostLabelling)
     633     ])
     634    (check_cost_program_ok p).
     635@(proj1 … H)
     636% qed.
     637
  • src/RTLabs/CostInj.ma

    r2937 r3022  
    11include "RTLabs/CostSpec.ma".
     2
     3(* This isn't quite right - it should be injective over all PCs, not just
     4   per-function. *)
    25
    36(* Check that the RTLabs pc → cost label map is injective for a given RTLabs
     
    128131λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f | _ ⇒ true ]) (prog_funct … p).
    129132
    130 theorem check_project_cost_injectivity_ok : ∀p.
     133theorem check_program_cost_injectivity_ok : ∀p.
    131134  bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p.
    132135#p %
     
    143146
    144147
     148definition check_program_cost_injectivity_prf : ∀p:RTLabs_program. res (program_cost_injectivity p) ≝
     149λp. (match check_program_cost_injectivity p return λb. bool_to_Prop b ↔ program_cost_injectivity p → res ? with
     150     [ true ⇒ λH. OK ??
     151     | false ⇒ λ_. Error ? (msg BadCostLabelling)
     152     ])
     153    (check_program_cost_injectivity_ok p).
     154@(proj1 … H)
     155% qed.
    145156
Note: See TracChangeset for help on using the changeset viewer.