Mefresa.GCM.Interface
Require Import Mefresa.GCM.Base.
An interface is constituted by a name, a signature, a path, a visibility,
a communication role, a functionality, a contingency and a cardinality.
The interface's name is an identifier as defined in Intro.v.
As for the remaining, we define them below, along with comparison operators,
and associate nice notations to it.
Signature
Definition signature := string.
Lemma signature_dec:
forall sig sig': signature, {sig = sig'} + {sig <> sig'}.
Proof.
repeat decide equality.
Qed.
Definition beq_signature : signature -> signature -> bool := beq_string.
Bind Scope signature_scope with signature.
Delimit Scope signature_scope with signature.
Notation "t1 '==' t2" := (beq_signature t1 t2) (at level 80) : signature_scope.
Notation "t1 '!=' t2" := (~~ beq_signature t1 t2) (at level 80) : signature_scope.
Lemma signature_eq_reflection:
forall s s', (s==s')%signature = true <-> s=s'.
Proof.
intros.
unfold beq_signature.
split; intro;
apply beq_string_reflection; auto.
Qed.
Inductive visibility : Type :=
| Internal : visibility
| External : visibility.
Function beq_visibility (v1 v2:visibility) : bool :=
match v1, v2 with
| Internal, Internal => true
| External, External => true
| _, _ => false
end.
Bind Scope vis_scope with visibility.
Delimit Scope vis_scope with vis.
Notation "v1 '==' v2" := (beq_visibility v1 v2) (at level 80) : vis_scope.
Notation "v1 '!=' v2" := (~~ beq_visibility v1 v2) (at level 80) : vis_scope.
For instance, we can prove some basic properties about the accessibility definition.
Lemma internal_or_external:
forall a : visibility, a = Internal \/ a = External.
Proof.
intros.
destruct a.
left; reflexivity.
right; reflexivity.
Qed.
Lemma visibility_dec:
forall a b : visibility, a=b \/ a <> b.
Proof.
intros.
decide equality.
Qed.
Lemma vis_equality_Prop2bool:
forall a a',
a = a' ->
(a == a')%vis = true.
Proof.
intros.
functional induction beq_visibility a a'; auto.
destruct v1; inversion y.
Qed.
Lemma vis_equality_Prop2bool':
forall a a',
a <> a' ->
(a == a')%vis = false.
Proof.
intros.
functional induction beq_visibility a a';
congruence.
Qed.
Lemma vis_equality_bool2Prop:
forall a a',
(a == a')%vis = false -> a <> a'.
Proof.
intros.
functional induction beq_visibility a a'; try
congruence.
destruct v1; destruct v2; inversion y; intuition; inversion H0.
Qed.
Lemma vis_equality_bool2Prop':
forall a a',
(a == a')%vis = true -> a = a'.
Proof.
intros.
functional induction beq_visibility a a'; auto.
congruence.
Qed.
Hint Resolve vis_equality_Prop2bool vis_equality_Prop2bool'
vis_equality_bool2Prop vis_equality_bool2Prop'.
Lemma visibility_eq_reflection:
forall v1 v2, (v1 == v2)%vis = true <-> v1 = v2.
Proof.
destruct v1; destruct v2; simpl; split; try congruence.
Qed.
Lemma vis_bool_conjunction_fact:
forall a a' X,
X && (a == a')%vis = true ->
(a == a')%vis = true.
Proof.
intros.
functional induction beq_visibility a a'; auto.
destruct v1; destruct v2; inversion y;
destruct X; simpl in *; congruence.
Qed.
Hint Resolve vis_bool_conjunction_fact.
forall a : visibility, a = Internal \/ a = External.
Proof.
intros.
destruct a.
left; reflexivity.
right; reflexivity.
Qed.
Lemma visibility_dec:
forall a b : visibility, a=b \/ a <> b.
Proof.
intros.
decide equality.
Qed.
Lemma vis_equality_Prop2bool:
forall a a',
a = a' ->
(a == a')%vis = true.
Proof.
intros.
functional induction beq_visibility a a'; auto.
destruct v1; inversion y.
Qed.
Lemma vis_equality_Prop2bool':
forall a a',
a <> a' ->
(a == a')%vis = false.
Proof.
intros.
functional induction beq_visibility a a';
congruence.
Qed.
Lemma vis_equality_bool2Prop:
forall a a',
(a == a')%vis = false -> a <> a'.
Proof.
intros.
functional induction beq_visibility a a'; try
congruence.
destruct v1; destruct v2; inversion y; intuition; inversion H0.
Qed.
Lemma vis_equality_bool2Prop':
forall a a',
(a == a')%vis = true -> a = a'.
Proof.
intros.
functional induction beq_visibility a a'; auto.
congruence.
Qed.
Hint Resolve vis_equality_Prop2bool vis_equality_Prop2bool'
vis_equality_bool2Prop vis_equality_bool2Prop'.
Lemma visibility_eq_reflection:
forall v1 v2, (v1 == v2)%vis = true <-> v1 = v2.
Proof.
destruct v1; destruct v2; simpl; split; try congruence.
Qed.
Lemma vis_bool_conjunction_fact:
forall a a' X,
X && (a == a')%vis = true ->
(a == a')%vis = true.
Proof.
intros.
functional induction beq_visibility a a'; auto.
destruct v1; destruct v2; inversion y;
destruct X; simpl in *; congruence.
Qed.
Hint Resolve vis_bool_conjunction_fact.
Inductive role : Type :=
| Client: role
| Server: role.
Function beq_role (co1 co2:role) : bool :=
match co1, co2 with
| Client, Client => true
| Server, Server => true
| _, _ => false
end.
Bind Scope role_scope with role.
Delimit Scope role_scope with role.
Notation "co1 '==' co2" := (beq_role co1 co2) (at level 80) : role_scope.
Notation "co1 '!=' co2" := (~~ beq_role co1 co2) (at level 80) : role_scope.
Lemma role_bool_prop:
forall co1 co2, (co1 == co2)%role = true <-> co1 = co2.
Proof.
split; intro.
Case "Bool to Prop".
destruct co1; destruct co2; auto;
try (compute in H; congruence).
Case "Prop to Bool".
destruct co1; destruct co2; auto;
congruence.
Qed.
Lemma role_eq_reflection :
forall co1 co2, (co1 == co2)%role = true <-> co1 = co2.
Proof.
split; intro.
Case "Bool to Prop".
destruct co1; destruct co2; auto;
try (compute in H; congruence).
Case "Prop to Bool".
destruct co1; destruct co2; auto;
congruence.
Qed.
Hint Resolve role_bool_prop.
Inductive functionality : Type :=
| Functional : functionality
| Control : functionality.
Function beq_functionality (f1 f2:functionality) : bool :=
match f1, f2 with
| Functional, Functional => true
| Control, Control => true
| _, _ => false
end.
Bind Scope func_scope with functionality.
Delimit Scope func_scope with func.
Notation "f1 '==' f2" := (beq_functionality f1 f2) (at level 80) : func_scope.
Notation "f1 '!=' f2" := (~~ beq_functionality f1 f2) (at level 80) : func_scope.
Lemma functionality_eq_reflection:
forall f f', (f==f')%func = true <-> f=f'.
Proof.
destruct f; destruct f'; simpl; split; try congruence.
Qed.
Inductive contingency : Type :=
| Optional : contingency
| Mandatory: contingency.
Function beq_contingency (cont1 cont2:contingency) : bool :=
match cont1, cont2 with
| Optional , Optional => true
| Mandatory, Mandatory => true
| _, _ => false
end.
Bind Scope cont_scope with contingency.
Delimit Scope cont_scope with cont.
Notation "cont1 '==' cont2" := (beq_contingency cont1 cont2) (at level 80) : cont_scope.
Notation "cont1 '!=' cont2" := (~~ beq_contingency cont1 cont2) (at level 80) : cont_scope.
Lemma contingency_eq_reflection:
forall c c', (c==c')%cont = true <-> c=c'.
Proof.
destruct c; destruct c'; simpl; split; try congruence.
Qed.
Inductive cardinality : Type :=
| Singleton : cardinality
| Collection: cardinality
| Multicast : cardinality
| Gathercast: cardinality.
Function beq_cardinality (card1 card2:cardinality) : bool :=
match card1, card2 with
| Singleton , Singleton => true
| Collection, Collection => true
| Multicast , Multicast => true
| Gathercast, Gathercast => true
| _ , _ => false
end.
Bind Scope card_scope with cardinality.
Delimit Scope card_scope with card.
Notation "card1 '==' card2" := (beq_cardinality card1 card2) (at level 80) : card_scope.
Notation "card1 '!=' card2" := (~~ beq_cardinality card1 card2) (at level 80) : card_scope.
Lemma cardinality_eq_reflection:
forall c c', (c==c')%card = true <-> c=c'.
Proof.
destruct c; destruct c'; simpl; split; try congruence.
Qed.
The intended meaning of the above definitions should be clear. An interface
is either accessible from the internal or external side of the component.
It can either receive or establish communications, i.e. a server or
client interface. Its purpose can be of controlling the component (also
referred to as non-functional), or may be providing some functionality.
...
Finnaly, we define the notion of interface. It essentially reassembles all
the previous definitions.
Inductive interface : Type :=
| Interface : ident ->
signature ->
path ->
visibility ->
role ->
functionality ->
contingency ->
cardinality ->
interface.
| Interface : ident ->
signature ->
path ->
visibility ->
role ->
functionality ->
contingency ->
cardinality ->
interface.
Having defined our interface element, we will need a comparison operator
over two interfaces. Not surprisingly, two interfaces are equal if all elements
are equal.
Function beq_interface (i i':interface) : bool :=
match i, i' with
| Interface id sig p a r f ct cd, Interface id' sig' p' a' r' f' ct' cd' =>
(id == id') && (sig == sig')%signature && (p == p')%path &&
(a == a')%vis && (r == r')%role && (f == f')%func &&
(ct == ct')%cont && (cd == cd')%card
end.
Bind Scope interface_scope with interface.
Delimit Scope interface_scope with int.
Notation "i1 '==' i2" := (beq_interface i1 i2) (at level 80) : interface_scope.
Notation "i1 '!=' i2" := (~~ beq_interface i1 i2) (at level 80) : interface_scope.
Lemma interface_dec:
forall i i' : interface, {i = i'} + {i <> i'}.
Proof.
intros.
repeat decide equality.
Qed.
Require Import Coq.Bool.Bool.
Lemma interface_eq_reflection:
forall i i':interface, i = i' <-> (i == i')%int = true.
Proof.
split; intro.
Case "Prop Entails Bool".
subst; simpl.
destruct i'. simpl.
repeat rewrite andb_true_iff.
repeat split; auto.
apply beq_string_reflection; auto.
apply role_bool_prop; auto.
apply functionality_eq_reflection; auto.
apply contingency_eq_reflection; auto.
apply cardinality_eq_reflection; auto.
Case "Bool Entails Prop".
destruct i; destruct i'.
simpl in H.
repeat rewrite andb_true_iff in H.
do 7 (destruct H).
rewrite role_bool_prop in H3.
rewrite functionality_eq_reflection in H2.
rewrite contingency_eq_reflection in H1.
rewrite cardinality_eq_reflection in H0.
rewrite visibility_eq_reflection in H4.
rewrite signature_eq_reflection in H6.
rewrite path_eq_reflection in H5.
rewrite ident_eq_reflection in H.
subst; auto.
Qed.
Definition projectionInterfaceId (i:interface) : ident :=
match i with
| Interface id t owner acc com func cont card => id
end.
Definition projectionInterfaceSignature (i:interface) : signature :=
match i with
| Interface id sig owner acc com func cont card => sig
end.
Definition projectionInterfaceOwner (i:interface) : path :=
match i with
| Interface id sig owner acc com func cont card => owner
end.
Definition projectionInterfaceRole (i:interface) : role :=
match i with
| Interface id sig owner acc com func cont card => com
end.
Definition projectionInterfaceVisibility (i:interface) : visibility :=
match i with
| Interface id sig owner vis com func cont card => vis
end.
Definition projectionInterfaceFunctionality (i:interface) : functionality :=
match i with
| Interface id sig owner acc com func cont card => func
end.
Definition projectionInterfaceContingency (i:interface) : contingency :=
match i with
| Interface id sig owner acc com func cont card => cont
end.
Definition projectionInterfaceCardinality (i:interface) : cardinality :=
match i with
| Interface id sig owner acc com func cont card => card
end.
Having the projections defined we will now use Coq's Notation capabilities in order
to define some operators that will make the readability much more convenient.
Notation "i '->id' " := (projectionInterfaceId i) (at level 80, right associativity) : interface_scope.
Notation "i '->sig' " := (projectionInterfaceSignature i) (at level 80, right associativity) : interface_scope.
Notation "i '->owner' " := (projectionInterfaceOwner i) (at level 80, right associativity) : interface_scope.
Notation "i '->visibility' " := (projectionInterfaceVisibility i) (at level 80, right associativity) : interface_scope.
Notation "i '->functionality' " := (projectionInterfaceFunctionality i) (at level 80, right associativity) : interface_scope.
Notation "i '->role' " := (projectionInterfaceRole i) (at level 80, right associativity) : interface_scope.
Notation "i '->contingency' " := (projectionInterfaceContingency i) (at level 80, right associativity) : interface_scope.
Notation "i '->cardinality' " := (projectionInterfaceCardinality i) (at level 80, right associativity) : interface_scope.
Bind Scope interface_scope with interface.
Delimit Scope interface_scope with int.
A few interface-related facts
Lemma beq_visibility_symmetry:
forall i i', ((i->visibility%int) == (i'->visibility%int))%vis = true <->
((i'->visibility%int) == (i->visibility%int))%vis = true.
Proof.
intros.
split; intro.
Case "Left entails right".
functional induction beq_visibility (i->visibility%int) (i'->visibility%int).
SCase "Both are Internal".
thus reflexivity.
SCase "Both are External".
thus reflexivity.
SCase "They are different".
congruence.
Case "Right entails left".
functional induction beq_visibility (i'->visibility%int) (i->visibility%int).
SCase "Idents are equal".
thus reflexivity.
SCase "Both are External".
thus reflexivity.
SCase "They are different".
congruence.
Qed.
Lemma inner_symmetry:
forall id id' a a',
(id == id') && (a == a')%vis = (id' == id) && (a' == a)%vis.
Proof.
intros.
destruct ident_dec with (id1:=id) (id2:=id');
destruct visibility_dec with (a:=a) (b:=a').
Case "1/4".
subst; refl.
Case "2/4".
assert ((a == a')%vis = false).
auto.
rewrite H0.
assert ((id == id') = true).
eauto.
rewrite H1.
assert ((a' == a)%vis = false).
eauto.
rewrite H2.
simpl.
assert ((id' == id) = true).
eauto.
rewrite H3;auto.
Case "3/4".
assert ((id' == id) = false).
eauto.
assert ((a == a')%vis = true).
eauto.
rewrite H0; rewrite H1.
assert ((id == id') = false).
apply beq_ident_symmetry.
auto.
rewrite H2.
simpl; auto.
Case "4/4".
assert ((id == id') = false).
eauto.
assert ((id' == id) = false).
eauto.
rewrite H0; rewrite H1; refl.
Qed.
Moreover, we shall also prove that fact that our beq_vis function
is reflexive.
Lemma beq_visibility_reflexivity:
forall a, (a == a)%vis = true.
Proof.
intro.
destruct a; reflexivity.
Qed.
The interfaces of some component might not have unique ids. Indeed, the only requirement
at this stage is that if two interfaces have the same id, then they must have different
accessibility values.
Let us define some functions to query over a list of interfaces.
Function interface_id_exists (id:ident) (l:list interface) {struct l} : bool :=
match l with
| nil => false
| i :: r => if ((i->id)%int == id) then
true
else
interface_id_exists id r
end.
Notation "l '[' id ']'" := (interface_id_exists id l) (at level 60, right associativity) : interface_scope.
Function get_interface (id:ident) (a:visibility)
(l:list interface) {struct l} : option interface :=
match l with
| nil => None
| i :: r => if ((i->id)%int == id) && ((i->visibility)%int == a)%vis then
Some i
else
get_interface id a r
end.
Notation "l '[' id ',' a ']'" := (get_interface id a l) (at level 60, right associativity) : interface_scope.
Function get_interface_vis_role_cont (v:visibility) (ro:role) (ct:contingency)
(li:list interface) {struct li} : list interface :=
match li with
nil => nil
| i :: r => if ((i->visibility%int) == v)%vis && ((i->role%int) == ro)%role &&
((i->contingency%int) == ct)%cont then
i :: get_interface_vis_role_cont v ro ct r
else
get_interface_vis_role_cont v ro ct r
end.
Notation "l '[' v ',' r ',' ct ']'" := (get_interface_vis_role_cont v r ct l) (at level 60, right associativity) : interface_scope.
Function get_interface_id_vis_role (id:ident) (v:visibility) (r:role)
(l:list interface) {struct l} : option interface :=
match l with
| nil => None
| i :: r' => if ((i->id)%int == id) &&
((i->visibility)%int == v)%vis && ((i->role)%int == r)%role then
Some i
else
get_interface_id_vis_role id v r r'
end.
Notation "l '[' id ',' v ',' r ']'" := (get_interface_id_vis_role id v r l) (at level 60, right associativity) : interface_scope.
Function get_interface_id_role (id:ident) (r:role)
(l:list interface) {struct l} : option interface :=
match l with
| nil => None
| i :: r' => if ((i->id)%int == id) && ((i->role)%int == r)%role then
Some i
else
get_interface_id_role id r r'
end.
Notation "l '[' id ';' r ']'" := (get_interface_id_role id r l) (at level 60, right associativity) : interface_scope.
Function get_interface_id_vis_role_cont (id:ident) (v:visibility) (r:role) (ct:contingency)
(l:list interface) {struct l} : option interface :=
match l with
| nil => None
| i :: r' => if ((i->id)%int == id) &&
((i->visibility)%int == v)%vis && ((i->role)%int == r)%role && ((i->contingency)%int == ct)%cont then
Some i
else
get_interface_id_vis_role_cont id v r ct r'
end.
Notation "l '[' id ',' v ',' r ',' ct ']'" := (get_interface_id_vis_role_cont id v r ct l) (at level 60, right associativity) : interface_scope.
The function interface_id_exists takes one identifier and a list of interfaces as
arguments. It returns true if there exists at least one interface whose identifier
is equal to the identifier passed as argument, and false otherwise.
As for the function get_interface it takes an identifier, an accessibility and a list
of interfaces. If it exists, it returns the interface that matches both the id
and accessibility fields.
Lemma interfaces_fact:
forall id l,
interface_id_exists id l = true ->
exists a,
exists x,
get_interface id a l = Some x.
Proof.
intros.
functional induction interface_id_exists id l.
Case "List is empty".
congruence.
Case "List is not empty, the provided id matches".
destruct i.
exists v.
exists (Interface i s p v r0 f c c0).
clear H.
unfold get_interface.
rewrite e0.
simpl.
assert ((v==v)%vis = true).
apply beq_visibility_reflexivity.
rewrite H.
reflexivity.
Case "List is not empty, the provided id does not match".
destruct i.
destruct IHb; auto.
destruct H0.
exists x.
exists x0.
simpl in *.
rewrite e0.
simpl.
apply H0.
Qed.