Ignore:
Timestamp:
Aug 10, 2011, 5:17:58 PM (9 years ago)
Author:
campbell
Message:

Show that RTLabs graphs are closed on branch (i.e., all labels in
instructions are in the graph). Rather time consuming and fiddly.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma

    r1071 r1105  
    2727.
    2828
     29definition labels_P : (label → Prop) → statement → Prop ≝
     30λP,s. match s with
     31[ St_skip l ⇒ P l
     32| St_cost _ l ⇒ P l
     33| St_const _ _ l ⇒ P l
     34| St_op1 _ _ _ l ⇒ P l
     35| St_op2 _ _ _ _ l ⇒ P l
     36| St_load _ _ _ l ⇒ P l
     37| St_store _ _ _ l ⇒ P l
     38| St_call_id _ _ _ l ⇒ P l
     39| St_call_ptr _ _ _ l ⇒ P l
     40| St_tailcall_id _ _ ⇒ True
     41| St_tailcall_ptr _ _ ⇒ True
     42| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
     43| St_jumptable _ ls ⇒ All ? P ls
     44| St_return ⇒ True
     45].
     46
     47lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s.
     48#P #Q #H * /3/
     49#r #l #l' * /3/
     50qed.
     51
     52definition labels_present : graph statement → statement → Prop ≝
     53λg,s. labels_P (present ?? g) s.
     54
     55definition graph_closed : graph statement → Prop ≝
     56λg. ∀l,s. lookup ?? g l = Some ? s → labels_present g s.
     57
    2958record internal_function : Type[0] ≝
    3059{ f_labgen    : universe LabelTag
     
    3564; f_stacksize : nat
    3665; f_graph     : graph statement
    37 ; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
    38 ; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
     66; f_closed    : graph_closed f_graph
     67; f_entry     : Σl:label. present ?? f_graph l
     68; f_exit      : Σl:label. present ?? f_graph l
    3969}.
    4070
Note: See TracChangeset for help on using the changeset viewer.