Interface
Require Import Intro.
An interface is constituted by an identifier, a type, an accessibility,
a communication role, a functionality and a language. The interface's
identifier is defined as was discussed in Intro.v. As for the remaining,
we define them below, along with comparison operators, and associate nice notations
to it.
Type
Inductive type : Type :=
| Int : type
| Bool : type
| Float : type
| Double : type
| Top : type.
Function beq_type (t1 t2:type) : bool :=
match t1, t2 with
| Int, Int => true
| Bool, Bool => true
| Float, Float => true
| Double, Double => true
| Top, Top => true
| _, _ => false
end.
Lemma type_dec:
forall t t': type, {t = t'} + {t <> t'}.
Proof.
decide equality.
Qed.
Bind Scope type_scope with type.
Delimit Scope type_scope with type.
Notation "t1 '==' t2" := (beq_type t1 t2) (at level 80) : type_scope.
Notation "t1 '!=' t2" := (~~ beq_type t1 t2) (at level 80) : type_scope.
Inductive accessibility : Type :=
| Internal : accessibility
| External : accessibility.
Function beq_accessibility (acc1 acc2:accessibility) : bool :=
match acc1, acc2 with
| Internal, Internal => true
| External, External => true
| _, _ => false
end.
Bind Scope acc_scope with accessibility.
Delimit Scope acc_scope with acc.
Notation "a1 '==' a2" := (beq_accessibility a1 a2) (at level 80) : acc_scope.
Notation "a1 '!=' a2" := (~~ beq_accessibility a1 a2) (at level 80) : acc_scope.
For instance, we can prove some basic properties about the accessibility definition.
Lemma internal_or_external:
forall a : accessibility, a = Internal \/ a = External.
Proof.
intros.
destruct a.
left; reflexivity.
right; reflexivity.
Qed.
Lemma access_dec:
forall a b : accessibility, a=b \/ a <> b.
Proof.
intros.
decide equality.
Qed.
Lemma acc_equality_Prop2bool:
forall a a',
a = a' ->
(a == a')%acc = true.
Proof.
intros.
functional induction beq_accessibility a a'; auto.
destruct acc1; inversion y.
Qed.
Lemma acc_equality_Prop2bool':
forall a a',
a <> a' ->
(a == a')%acc = false.
Proof.
intros.
functional induction beq_accessibility a a';
congruence.
Qed.
Lemma acc_equality_bool2Prop:
forall a a',
(a == a')%acc = false -> a <> a'.
Proof.
intros.
functional induction beq_accessibility a a'; try
congruence.
destruct acc1; destruct acc2; inversion y; intuition; inversion H0.
Qed.
Lemma acc_equality_bool2Prop':
forall a a',
(a == a')%acc = true -> a = a'.
Proof.
intros.
functional induction beq_accessibility a a'; auto.
congruence.
Qed.
Hint Resolve acc_equality_Prop2bool acc_equality_Prop2bool'
acc_equality_bool2Prop acc_equality_bool2Prop'.
Lemma acc_bool_conjunction_fact:
forall a a' X,
X && (a == a')%acc = true ->
(a == a')%acc = true.
Proof.
intros.
functional induction beq_accessibility a a'; auto.
destruct acc1; destruct acc2; inversion y;
destruct X; simpl in *; congruence.
Qed.
Hint Resolve acc_bool_conjunction_fact.
forall a : accessibility, a = Internal \/ a = External.
Proof.
intros.
destruct a.
left; reflexivity.
right; reflexivity.
Qed.
Lemma access_dec:
forall a b : accessibility, a=b \/ a <> b.
Proof.
intros.
decide equality.
Qed.
Lemma acc_equality_Prop2bool:
forall a a',
a = a' ->
(a == a')%acc = true.
Proof.
intros.
functional induction beq_accessibility a a'; auto.
destruct acc1; inversion y.
Qed.
Lemma acc_equality_Prop2bool':
forall a a',
a <> a' ->
(a == a')%acc = false.
Proof.
intros.
functional induction beq_accessibility a a';
congruence.
Qed.
Lemma acc_equality_bool2Prop:
forall a a',
(a == a')%acc = false -> a <> a'.
Proof.
intros.
functional induction beq_accessibility a a'; try
congruence.
destruct acc1; destruct acc2; inversion y; intuition; inversion H0.
Qed.
Lemma acc_equality_bool2Prop':
forall a a',
(a == a')%acc = true -> a = a'.
Proof.
intros.
functional induction beq_accessibility a a'; auto.
congruence.
Qed.
Hint Resolve acc_equality_Prop2bool acc_equality_Prop2bool'
acc_equality_bool2Prop acc_equality_bool2Prop'.
Lemma acc_bool_conjunction_fact:
forall a a' X,
X && (a == a')%acc = true ->
(a == a')%acc = true.
Proof.
intros.
functional induction beq_accessibility a a'; auto.
destruct acc1; destruct acc2; inversion y;
destruct X; simpl in *; congruence.
Qed.
Hint Resolve acc_bool_conjunction_fact.
Inductive communication : Type :=
| Client: communication
| Server: communication.
Function beq_communication (co1 co2:communication) : bool :=
match co1, co2 with
| Client, Client => true
| Server, Server => true
| _, _ => false
end.
Bind Scope com_scope with communication.
Delimit Scope com_scope with com.
Notation "co1 '==' co2" := (beq_communication co1 co2) (at level 80) : com_scope.
Notation "co1 '!=' co2" := (~~ beq_communication co1 co2) (at level 80) : com_scope.
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.
Inductive language : Type :=
| Idl : language
| C : language
| Java : language.
Function beq_language (l1 l2:language) : bool :=
match l1, l2 with
| Idl, Idl => true
| C, C => true
| Java, Java => true
| _, _ => false
end.
Bind Scope lang_scope with language.
Delimit Scope lang_scope with lang.
Notation "l1 '==' l2" := (beq_language l1 l2) (at level 80) : lang_scope.
Notation "l1 '!=' l2" := (~~ beq_language l1 l2) (at level 80) : lang_scope.
The intended meaning of the above definitions should be clear. An interface's
type maps directly to a type one would find in a standard programming language.
It 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.
At last, it implements a language.
The above definitions are not sufficient to model an interface. Indeed,
the GCM Component Model is an hierarchical component model. The way we
encode this shall be discussed later, but for now we can focus on the fact
that in order to identify an interface we need to locate it in the hierarchy.
Therefore, we need another field indicating its position, we shall call it
path.
Path
Naturaly, two paths are equal if all identifiers constituting them are equal.
Function beq_path (p p':path) {struct p} : bool :=
match p, p' with
| nil, nil => true
| id :: r, id' :: r' => if (id != id') then false else beq_path r r'
| _, _ => false
end.
Bind Scope path_scope with path.
Delimit Scope path_scope with path.
Notation "p1 '==' p2" := (beq_path p1 p2) (at level 80) : path_scope.
Notation "p1 '!=' p2" := (~~ beq_path p1 p2) (at level 80) : path_scope.
Finnaly, we define the notion of interface. It essentially reassembles all
the previous definitions.
Inductive interface : Type :=
| Interface : ident ->
type ->
path ->
accessibility ->
communication ->
functionality ->
language ->
interface.
| Interface : ident ->
type ->
path ->
accessibility ->
communication ->
functionality ->
language ->
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 t p a c f l, Interface id' t' p' a' c' f' l' =>
(id == id') && (t == t')%type && (p == p')%path &&
(a == a')%acc && (c == c')%com && (f == f')%func && (l == l')%lang
end.
Lemma interface_dec:
forall i i' : interface, {i = i'} + {i <> i'}.
Proof.
intros.
decide equality; decide equality.
Qed.
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.
Definition projectionInterfaceId (i:interface) : ident :=
match i with
| Interface id t owner acc com func language => id
end.
Definition projectionInterfaceType (i:interface) : type :=
match i with
| Interface id t owner acc com func language => t
end.
Definition projectionInterfaceOwner (i:interface) : path :=
match i with
| Interface id t owner acc com func language => owner
end.
Definition projectionInterfaceCommunication (i:interface) : communication :=
match i with
| Interface id t owner acc com func language => com
end.
Definition projectionInterfaceLanguage (i:interface) : language :=
match i with
| Interface id t owner acc com func language => language
end.
Definition projectionInterfaceAccessibility (i:interface) : accessibility :=
match i with
| Interface id t owner acc com func language => acc
end.
Definition projectionInterfaceFunctionality (i:interface) : functionality :=
match i with
| Interface id t owner acc com func language => func
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 '->type' " := (projectionInterfaceType i) (at level 80, right associativity) : interface_scope.
Notation "i '->owner' " := (projectionInterfaceOwner i) (at level 80, right associativity) : interface_scope.
Notation "i '->language' " := (projectionInterfaceLanguage i) (at level 80, right associativity) : interface_scope.
Notation "i '->accessibility' " := (projectionInterfaceAccessibility i) (at level 80, right associativity) : interface_scope.
Notation "i '->functionality' " := (projectionInterfaceFunctionality i) (at level 80, right associativity) : interface_scope.
Notation "i '->com' " := (projectionInterfaceCommunication i) (at level 80, right associativity) : interface_scope.
Bind Scope interface_scope with interface.
Delimit Scope interface_scope with int.
For instance, if we wanted the prove the symmetry of our beq_acc function,
we could express it by recurring to the following syntactic sugar.
Lemma beq_accessibility_symmetry:
forall i i', ((i->accessibility%int) == (i'->accessibility%int))%acc = true <->
((i'->accessibility%int) == (i->accessibility%int))%acc = true.
Proof.
intros.
split; intro.
Case "Left entails right".
functional induction beq_accessibility (i->accessibility%int) (i'->accessibility%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_accessibility (i'->accessibility%int) (i->accessibility%int).
SCase "Idents are equal".
thus reflexivity.
SCase "Both are External".
thus reflexivity.
SCase "They are different".
congruence.
Qed.
Lemma access_equality_Prop2bool':
forall a a' : accessibility,
a <> a' ->
(a == a')%acc = false.
Proof.
intros.
functional induction beq_accessibility a a';
congruence.
Qed.
Lemma access_equality_Prop2bool:
forall a a' : accessibility,
a = a' ->
(a == a')%acc = true.
Proof.
intros.
functional induction beq_accessibility a a';
auto.
induction acc1; inversion y.
Qed.
Hint Resolve access_equality_Prop2bool access_equality_Prop2bool'.
Lemma inner_symmetry:
forall id id' a a',
(id == id') && (a == a')%acc = (id' == id) && (a' == a)%acc.
Proof.
intros.
destruct ident_dec with (id1:=id) (id2:=id');
destruct access_dec with (a:=a) (b:=a').
Case "1/4".
subst; refl.
Case "2/4".
assert ((a == a')%acc = false).
auto.
rewrite H0.
assert ((id == id') = true).
eauto.
rewrite H1.
assert ((a' == a)%acc = false).
eauto.
rewrite H2.
simpl.
assert ((id' == id) = true).
eauto.
rewrite H3;auto.
Case "3/4".
assert ((id' == id) = false).
eauto.
assert ((a == a')%acc = 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_acc function
is reflexive.
Lemma beq_accessibility_reflexivity:
forall a, (a == a)%acc = 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:accessibility)
(l:list interface) {struct l} : option interface :=
match l with
| nil => None
| i :: r => if ((i->id)%int == id) && ((i->accessibility)%int == a)%acc 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.
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 a.
exists (Interface i t p a c f l).
clear H.
unfold get_interface.
rewrite e0.
simpl.
assert ((a==a)%acc = true).
apply beq_accessibility_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.