Changeset 3500 for LTS/costs.ma


Ignore:
Timestamp:
Sep 25, 2014, 6:50:51 PM (6 years ago)
Author:
sacerdot
Message:

Nicer statements.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/costs.ma

    r3458 r3500  
    4343}.
    4444
    45 record galois_conn (C : concrete_transition_sys)
     45notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
     46interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
     47
     48record galois_rel (C : concrete_transition_sys)
    4649                   (A : abstract_transition_sys (cost_mon C)) : Type[0] ≝
    4750{ rel_galois :2> C → A → Prop
    4851; rel_galois_cost : ∀s,a.rel_galois … s a → abs_cost … a = cost_of … s
    49 ; rel_galois_prop : ∀s,s' : C.∀a : A.∀l.as_execute … l s s' → rel_galois … s a →
    50                     ∃i : abs_instr … A.∃a' : A.rel_galois … s' a' ∧
    51                                                act_abs ?? i a = a'
    5252}.
    5353
    54 record static_analysis_data : Type[2] ≝
     54record galois_connection : Type[2] ≝
    5555{ concr : concrete_transition_sys
    5656; abs_d : abstract_transition_sys (cost_mon concr)
    57 ; instr_t : Type[0]
    58 ; fetch : concr → option instr_t
    59 ; instr_map : instr_t → abs_instr … abs_d
     57; galois_rel:> galois_rel concr abs_d
    6058}.
    6159
    62 
    63 record static_galois (p : static_analysis_data) : Type[0] ≝
    64 { good :> galois_conn (concr … p) (abs_d … p)
    65 ; instr_map_ok : ∀s,s' : (concr … p).∀a : (abs_d … p).∀l,i.as_execute … l s s' →
    66                 fetch … p s = Some ? i →
    67                 rel_galois … good s a →
    68                 rel_galois … good s' (act_abs … (instr_map … p i) a)
     60record abstract_interpretation : Type[2] ≝
     61{ galois_conn:> galois_connection
     62; instr_t : Type[0]
     63; fetch : concr galois_conn → option instr_t
     64; instr_map : instr_t → abs_instr … (abs_d galois_conn)
     65; instr_map_ok :
     66   ∀s,s': concr … galois_conn. ∀a: abs_d … galois_conn.∀l,i.
     67    as_execute … l s s' →
     68     fetch … s = Some ? i →
     69      ∀I. instr_map … i = I →
     70       galois_conn s a → galois_conn s' (〚I〛 a)
    6971}.
    70 
    71 
    72 
    73 
Note: See TracChangeset for help on using the changeset viewer.