Mefresa.GCM.GCMTyping
Require Export Mefresa.GCM.CoreElementsFacts.
From the technical specification ETSI TS 102 830 v1.1.1, it is defined
the typing rules for running components. In this module we mechanize
this type system.
From the specification we know that the operations from Mandatory interfaces
must be guaranteed when a component is running. This is expected for Server
interfaces. However, for Client interfaces, since it does not have a functionality
of its own, we must ensure that it is indeed bound to a Mandatory Server interface.
Component Interfaces Contingency and Cardinality
Into Contingency - Client Mandatory Interfaces are Bound
Function get_normal_binding_recipients_aux (idC1 : ident) (idI1 : ident) (lb : list binding) : list (ident * ident) :=
match lb with
nil => nil
| Normal p idC1' idI1' idC2 idI2 :: r => if (idC1 == idC1')%id && (idI1 == idI1')%id then
(idC2, idI2) :: get_normal_binding_recipients_aux idC1 idI1 r
else
get_normal_binding_recipients_aux idC1 idI1 r
| _ :: r => get_normal_binding_recipients_aux idC1 idI1 r
end.
Function get_normal_binding_recipients_aux2 (lid : list (ident * ident)) (lc : list component) : (list interface) :=
match lid with
nil => nil
| (idC2, idI2) :: r => match lc[idC2] with
None => get_normal_binding_recipients_aux2 r lc
| Some c => match get_interface_id_role idI2 Server (c->interfaces%comp) with
None => get_normal_binding_recipients_aux2 r lc
| Some i => i :: get_normal_binding_recipients_aux2 r lc
end
end
end.
Function remove_components_without_interfaces lc : list component :=
match lc with
nil => nil
| c :: r => if ((c->interfaces%comp) == nil)%l_int then
remove_components_without_interfaces r
else
c :: remove_components_without_interfaces r
end.
Function get_normal_binding_recipients (idC1 : ident) (idI1 : ident)
(lb : list binding) (lc : list component) : list interface :=
match get_normal_binding_recipients_aux idC1 idI1 lb with
nil => nil
| lid => get_normal_binding_recipients_aux2 lid lc
end.
Function get_import_binding_recipients (idC : ident) (idIc : ident) (lb : list binding) (li : list interface) : list interface :=
match lb with
| nil => nil
| Import p idI idSubC idSubI :: r => if (idSubC == idC)%id && (idIc == idSubI)%id then
match (li[idI, Internal, Server])%int with
None => (get_import_binding_recipients idC idIc r li)
| Some i => i :: (get_import_binding_recipients idC idIc r li)
end
else
(get_import_binding_recipients idC idIc r li)
| _ :: r => (get_import_binding_recipients idC idIc r li)
end.
Inductive subcomponents_client_external_mandatory_interfaces_are_bound (c:component) : Prop :=
| CEMI_Bound: (forall c', In c' (c->subComponents%comp) ->
(forall int, In int (c'->interfaces%comp) ->
(int->role%int) = Client ->
(int->visibility%int) = External ->
(int->contingency%int) = Mandatory ->
((app (get_normal_binding_recipients (c'->id%comp) (int->id%int) (c->bindings%comp) (c->subComponents%comp))
(get_import_binding_recipients (c'->id%comp) (int->id%int) (c->bindings%comp) (c->interfaces%comp))) <> nil) /\
forall i, In i (app (get_normal_binding_recipients (c'->id%comp) (int->id%int) (c->bindings%comp) (c->subComponents%comp))
(get_import_binding_recipients (c'->id%comp) (int->id%int) (c->bindings%comp) (c->interfaces%comp))) ->
(i->contingency)%int = Mandatory
)) ->
(forall c', In c' (c->subComponents%comp) ->
subcomponents_client_external_mandatory_interfaces_are_bound c')
->
subcomponents_client_external_mandatory_interfaces_are_bound c.
Lemma primitive_are_internally_bounded:
forall id p cl li lb,
subcomponents_client_external_mandatory_interfaces_are_bound (Component id p default_class cl nil li lb).
Proof.
intros.
apply CEMI_Bound; intros.
Case "External Mandatory Interfaces Are bound".
simpl in *.
fromfalse.
Case "Recursive Call".
simpl in *.
fromfalse.
Qed.
Hint Resolve primitive_are_internally_bounded.
Function get_export_binding_recipients_aux (idI : ident) (lb : list binding) : list (ident * ident) :=
match lb with
nil => nil
| Export p idI' idSub idSubI :: r => if(idI == idI')%id then
(idSub, idSubI) :: get_export_binding_recipients_aux idI r
else
get_export_binding_recipients_aux idI r
| _ :: r => get_export_binding_recipients_aux idI r
end.
Function get_export_binding_recipients_aux2 (lid : list (ident * ident)) (lc: list component) : list interface :=
match lid with
nil => nil
| (idSub, idSubI) :: r => match lc[idSub] with
None => nil
| Some c => match (c->interfaces%comp)[idSubI, External, Server]%int with
None => nil
| Some i => i :: get_export_binding_recipients_aux2 r lc
end
end
end.
Function get_export_binding_recipients (idI: ident) (lb: list binding) (lc:list component) : list interface :=
match get_export_binding_recipients_aux idI lb with
nil => nil
| l => get_export_binding_recipients_aux2 l lc
end.
Inductive client_internal_mandatory_interfaces_are_bound (c: component) : Prop :=
| CIMI_Bound: (forall int, In int (c->interfaces%comp) ->
(int->role%int) = Client ->
(int->visibility%int) = Internal ->
(int->contingency%int) = Mandatory ->
(get_export_binding_recipients (int->id)%int (c->bindings%comp) (c->subComponents%comp) <> nil) /\
(forall i,
In i ((get_export_binding_recipients (int->id)%int (c->bindings%comp) (c->subComponents%comp))) ->
(i->contingency%int) = Mandatory
)
) ->
(forall c', In c' (c->subComponents%comp) ->
client_internal_mandatory_interfaces_are_bound c') ->
client_internal_mandatory_interfaces_are_bound c.
Definition client_internal_mandatory_itfs_are_bound :=
client_internal_mandatory_interfaces_are_bound.
The predicate client_internal_mandatory_interfaces_are_bound determines
whether a component has all its client-internal-mandatory interfaces
bound. On the other hand, the predicate subcomponents_client_external_mandatory_interfaces_are_bound
determines if all client-external-mandatory interfaces of a component's subcomponents are bound.
These two predicates together account for all interfaces of some component architecture.
Definition mandatory_interfaces_are_bound (s:component) : Prop :=
subcomponents_client_external_mandatory_interfaces_are_bound s /\
client_internal_mandatory_interfaces_are_bound s.
Let's see it at work.
Example interfaces_in_example_are_bound:
mandatory_interfaces_are_bound Primitive.
Proof.
unfold Primitive.
split; split; simpl; intros; try fromfalse.
destruct H as [Ha | [ Hb | [ Hc | [ Hd | [ He | Hf ]]]]];
subst; simpl in *; try congruence.
fromfalse.
Qed.
Our Primitive component example easily meets
this property as it has no bindings. For our Composite
component however, we are not able to establish it as
it does not contain all interfaces bound properly.
Indeed, a well_formed_component maybe not adhere to
the typing requirement.
From the specification ...
While checking for the Contingency we already make sure that
all interfaces that need to be bound, indeed are. Here, we only
need to check if all bindings are respecting the Cardinality
value of the involved interfaces
Into Cardinality
Inductive client_singleton_are_bound_once_at_most_export_bindings c : Prop :=
| SingletonExport:
(forall i, In i (c->interfaces%comp) ->
(i->role%int) = Client ->
(i->visibility%int) = Internal ->
(i->cardinality%int) = Singleton ->
( length ((get_export_binding_recipients (i->id)%int (c->bindings%comp) (c->subComponents%comp))) <= 1
)) ->
(forall c', In c' (c->subComponents%comp)->
client_singleton_are_bound_once_at_most_export_bindings c'
) ->
client_singleton_are_bound_once_at_most_export_bindings c.
Inductive client_singleton_are_bound_once_at_most_normal_import_bindings c : Prop :=
| SingletonNormalImport:
(forall c', In c' (c->subComponents%comp) ->
(forall int, In int (c'->interfaces%comp) ->
(int->role%int) = Client ->
(int->visibility%int) = External ->
(int->cardinality%int) = Singleton ->
(length (app (get_normal_binding_recipients (c'->id%comp) (int->id%int) (c->bindings%comp) (c->subComponents%comp))
(get_import_binding_recipients (c'->id%comp) (int->id%int) (c->bindings%comp) (c->interfaces%comp))) <= 1))) ->
(forall c', In c' (c->subComponents%comp) ->
client_singleton_are_bound_once_at_most_normal_import_bindings c') ->
client_singleton_are_bound_once_at_most_normal_import_bindings c.
Definition isServerExternalSingleton (i:interface) : Prop :=
(i ->role)%int = Server /\
(i ->visibility)%int = External /\
(i ->cardinality)%int = Singleton.
Definition isServerInternalSingleton (i:interface) : Prop :=
(i ->role)%int = Server /\
(i ->visibility)%int = Internal /\
(i ->cardinality)%int = Singleton.
Function get_connected_clients_ids_from_interface_normal_export ci ii lb : list ident :=
match lb with
nil => nil
| Export _ ii1 ic2 ii2 :: r => if (ci == ic2)%id && (ii == ii2)%id then
ii1 :: get_connected_clients_ids_from_interface_normal_export ci ii r
else
get_connected_clients_ids_from_interface_normal_export ci ii r
| Normal _ ic1 ii1 ic2 ii2 :: r => if (ci == ic2)%id && (ii == ii2)%id then
ii1 :: get_connected_clients_ids_from_interface_normal_export ci ii r
else
get_connected_clients_ids_from_interface_normal_export ci ii r
| _ :: r => get_connected_clients_ids_from_interface_normal_export ci ii r
end.
Function get_connected_clients_ids_from_interface_import ii lb : list ident :=
match lb with
nil => nil
| Import _ iis icc iic :: r => if (ii == iis)%id then
icc :: get_connected_clients_ids_from_interface_import ii r
else
get_connected_clients_ids_from_interface_import ii r
| _ :: r => get_connected_clients_ids_from_interface_import ii r
end.
Inductive server_singleton_are_bound_once_at_most c : Prop :=
| ServerSingleton:
(forall c', In c' (c->subComponents%comp) ->
forall i, In i (c'->interfaces%comp) ->
isServerExternalSingleton i ->
length (get_connected_clients_ids_from_interface_normal_export (c'->id%comp) (i->id%int) (c->bindings%comp)) <= 1) ->
(forall i, In i (c->interfaces%comp) ->
isServerInternalSingleton i ->
length (get_connected_clients_ids_from_interface_import (i->id%int) (c->bindings%comp)) <= 1) ->
(forall c', In c' (c->subComponents%comp) ->
server_singleton_are_bound_once_at_most c'
) ->
server_singleton_are_bound_once_at_most c.
Definition client_singleton_are_bound_once_at_most c : Prop :=
client_singleton_are_bound_once_at_most_export_bindings c /\
client_singleton_are_bound_once_at_most_normal_import_bindings c.
Definition sound_cardinality c : Prop :=
client_singleton_are_bound_once_at_most c .
Definition sound_contingency := mandatory_interfaces_are_bound.
Definition well_typed c : Prop :=
sound_cardinality c /\ sound_contingency c.