Subsets





Definition Subset (X : Type) := X -> Prop.




Definition Contained (X : Type) (X1 X2 : Subset X) :=

  forall x, X1 x -> X2 x.




Definition eq_Subset (X : Type) (X1 X2 : Subset X) :=

  Contained X X1 X2 /\ Contained X X2 X1.




Definition Union (X : Type) (X1 X2 : Subset X) (x : X) := X1 x \/ X2 x.




Definition Intersect (X : Type) (X1 X2 : Subset X) (x : X) := X1 x /\ X2 x.




Definition Emptyset (X : Type) (x : X) := False.




Definition eq_ext (A B : Type) (f g : A -> B) :=

  forall a, f a = g a.

Definitions

Variables and Events





Parameter Var : Set.

Axiom Var_dec : forall x y : Var, {x = y} + {x <> y}.

Parameter Event : Set.

Axiom Event_dec : forall e e' : Event, {e = e'} + {e <> e'}.




Definition Object := Var + Event.

Values





Parameter Val : Set.

Axiom Val_dec : forall x y : Val, {x = y} + {x <> y}.

Configurations





Parameter Conf : Set.

Axiom Conf_dec : forall c c' : Conf, {c = c'} + {c <> c'}.

Environments





Definition Memory := Var -> Val.

Definition eq_Memory := eq_ext Var Val.




Definition update (m : Memory) (x : Var) (v : Val) : Memory :=

  fun y : Var => match Var_dec x y with

    | left _ => v

    | right _ => m y

  end.

Transfert functions





Definition Phi := (Conf * Memory) -> (Conf * (Subset Event) * Memory) -> Prop.

Axiom Phi_dec : forall phi : Phi, forall (a : Conf * Memory)

                                         (a' : Conf * (Subset Event) * Memory),

                  phi a a' \/ ~ phi a a'.




Definition eq_Phi (phi phi' : Phi) := forall a a', (phi a a' <-> phi' a a').

Processes





Record Process : Type := mkProcess

  { R : Subset Object ;

    W : Subset Object ;

    C : Subset Conf   ;

    phi : Phi }.

Systems





Record System : Type := mkSystem

  { L : Subset Object ;

    P : Subset Process }.

Variables and Events read by a System


Definition Sys_Read (S : System) (o : Object) : Prop :=

  exists p, S.(P) p /\ p.(R) o.

Variables and Events written by a System


Definition Sys_Write (S : System) (o : Object) : Prop :=

  exists p, S.(P) p /\ p.(W) o.

Events of a System


Definition Sys_Events (S : System) (e : Event) : Prop :=

  Sys_Read S (inr Var e) \/ Sys_Write S (inr Var e).

Variables of a System


Definition Sys_Vars (S : System) (x : Var) : Prop :=

  Sys_Read S (inl Event x) \/ Sys_Write S (inl Event x).

Variables and Events of a System


Definition Sys_Objects (S : System) : Object -> Prop :=

  Union Object (Sys_Read S) (Sys_Write S).

Encapsulation and Assembly





Definition Encapsulation (S : System) (X : Subset Object) : System :=

  mkSystem X S.(P).




Definition Assembly (S1 S2 : System) : System :=

  mkSystem (Union Object S1.(L) S2.(L)) (Union Process S1.(P) S2.(P)).

Semantics





Record SysConf : Type := mkSysConf

  { Cs : Process -> Conf ;

    E  : Subset Event }.




Record State : Type := mkState

  { r : SysConf ;

    m : Memory }.




Definition Trace := nat -> State.




Parameter Sched : SysConf -> SysConf -> Prop. 

Inductive Transition (S : System) (st st' : State) : Prop :=

| Univers_Trans :

    

    (forall p, S.(P) p -> (st.(r).(Cs) p) = (st'.(r).(Cs) p)) ->

    (forall e, S.(L) (inr Var e)   -> (st.(r).(E) e <-> st'.(r).(E) e)) ->

    (forall x, S.(L) (inl Event x) -> (st.(m) x = st'.(m) x)) ->

      Transition S st st'

| Local_Trans :

    

    forall p E_p,

      S.(P) p ->

      p.(phi) (st.(r).(Cs) p, st.(m)) (st'.(r).(Cs) p, E_p, st'.(m)) ->

      (forall p', p' <> p -> st.(r).(Cs) p' = st'.(r).(Cs) p') ->

      eq_Subset Event st'.(r).(E) (Union Event st.(r).(E) E_p) ->

        Transition S st st'

| Sched_Trans :

    

    Sched st.(r) st'.(r) -> eq_Memory st.(m) st'.(m) ->

      Transition S st st'.




Definition Sem (S : System) (t : Trace) : Prop :=

  forall i, Transition S (t i) (t (i+1)%nat).

Read and Written Variables and Events

Semantically Read Variables by a Process


Definition Proc_Sem_Read_Var (p : Process) (x : Var) : Prop :=

  exists c : Conf, exists m : Memory,

  exists c' : Conf, exists E' : Subset Event, exists m' : Memory,

  exists v : Val,

    p.(C) c /\ p.(C) c' /\ p.(phi) (c, m) (c', E', m') /\

    ~ (p.(phi) (c, update m x v) (c', E', m')).

Semantically Read Events by a Process


Definition Proc_Sem_Read_Event (p : Process) (e : Event) : Prop :=

  exists C1  : Process -> Conf, exists E1  : Subset Event,

  exists C2 : Process -> Conf, exists E2 : Subset Event,

    p.(C) (C1 p) /\ p.(C) (C2 p) /\

    Sched (mkSysConf C1 (fun e' => ((e' = e) \/ E1 e')))

          (mkSysConf C2 E2) /\

    forall (C3 C4 : Process -> Conf) (E4 : Subset Event),

      C3 p = C1 p -> Sched (mkSysConf C3 E1) (mkSysConf C4 E4) ->

        C4 p <> C2 p.

Semantically Written Variables by a Process


Definition Proc_Sem_Write_Var (p : Process) (x : Var) : Prop :=

  exists c : Conf, exists m : Memory,

  exists c' : Conf, exists E' : Subset Event, exists m' : Memory,

    p.(C) c /\ p.(C) c' /\ p.(phi) (c, m) (c', E', m') /\ m x <> m' x.

Semantically Written Events by a Process


Definition Proc_Sem_Write_Event (p : Process) (e : Event) : Prop :=

  exists c : Conf, exists m : Memory,

  exists c' : Conf, exists E' : Subset Event, exists m' : Memory,

    p.(C) c /\ p.(C) c' /\ p.(phi) (c, m) (c', E', m') /\ E' e.

Semantically Read Variables and Events by a Process


Definition Proc_Sem_Read (p : Process) (o : Object) : Prop :=

  match o with

| inl x => Proc_Sem_Read_Var p x

| inr e => Proc_Sem_Read_Event p e

end.

Semantically Written Variables and Events by a Process


Definition Proc_Sem_Write (p : Process) (o : Object) : Prop :=

  match o with

| inl x => Proc_Sem_Write_Var p x

| inr e => Proc_Sem_Write_Event p e

end.

Semantically Read Variables and Events by a System


Definition Sys_Sem_Read (S : System) (o : Object) : Prop :=

  exists p, S.(P) p /\ Proc_Sem_Read p o.

Semantically Written Variables and Events by a System


Definition Sys_Sem_Write (S : System) (o : Object) : Prop :=

  exists p, S.(P) p /\ Proc_Sem_Write p o.

Well-formed Processes





Definition Is_Process (p : Process) : Prop :=

  (Contained Object (Proc_Sem_Read p) p.(R)) /\

  (Contained Object (Proc_Sem_Write p) p.(W)) /\

  (forall (c c' : Conf) (m m' : Memory) (E : Subset Event),

    p.(phi) (c, m) (c', E, m') -> p.(C) c /\ p.(C) c').

Well-formed Systems





Definition Is_System (S : System) : Prop :=

  forall p, S.(P) p -> Is_Process p.

Assembly condition





Definition Assemblable (S S' : System) : Prop :=

  eq_Subset Object (Intersect Object S.(L) (Sys_Write S')) (Emptyset Object) /\

  eq_Subset Object (Intersect Object S'.(L) (Sys_Write S)) (Emptyset Object) /\

  eq_Subset Process (Intersect Process S.(P) S'.(P)) (Emptyset Process).

Encapsulation Theorem





Theorem Encapsulation_Sem :

  forall (S : System) (X Y : Subset Object), Is_System S ->

    Contained Trace (Sem (Encapsulation S (Union Object X Y)))

                    (Sem (Encapsulation S X)).

Assembly Theorem





Theorem Assembly_Sem :

  forall (S S' : System), Is_System S -> Is_System S' -> Assemblable S S' ->

    eq_Subset Trace (Sem (Assembly S S')) (Intersect Trace (Sem S) (Sem S')).

Global Index