Mefresa.Examples.ParamSpec



Require Export Mefresa.Operation.Compliance.

Symmetric Interfaces


Definition symmetric_role r : role :=
  match r with
    Client => Server
  | Server => Client
  end.

Definition symmetric_visibility v : visibility :=
  match v with
    Internal => External
  | External => Internal
  end.

Notation "sym- r" := (symmetric_role r) (at level 80, right associativity) : role_scope.
Notation "sym- v" := (symmetric_visibility v) (at level 80, right associativity) : vis_scope.

Definition Mk_symmetric_interface id sig p v r f cont card : operation :=
  Mk_interface id sig p v r f cont card ;
  Mk_interface id sig p (sym- v)%vis (sym- r)%role f cont card.

Parametrized Operations

Being able to cope with parametrized specifications requires the ability to generate components. Before moving to this, we shall start by defining a function that suffixes a natural number to a given identifier.

Function suffix_ident (id:ident) (n:nat) : ident :=
  match id with
    | Ident str => Ident (append str (nat_to_string n))
  end.

Lemma app_str_yield_different_str:
  forall s n m, n <> m ->
                 (s ++ (nat_to_string n)) <> (s ++ (nat_to_string m)).
Proof.
  intros.
  assert (nat_to_string n <> nat_to_string m).
    apply nat_to_string_fact; auto.
  apply string_append_fact'; auto.
Qed.

Lemma suffix_ident_spec:
  forall n m id,
  n <> m ->
  suffix_ident id n <> suffix_ident id m.
Proof.
 intros.
 unfold suffix_ident.
 destruct id.
 assert ((s ++ (nat_to_string n)) <> (s ++ (nat_to_string m))).
   apply app_str_yield_different_str with (s:=s) (n:=n) (m:=m); auto.
 destruct ident_dec with (id1:=Ident(s ++ nat_to_string n))
                         (id2:=Ident(s ++ nat_to_string m)).
 Case "They are equal".
   inversion e. congruence.
 Case "They are not equal".
   auto.
Qed.
The above function suffix_ident is fairly simple, further its specification is given by the lemma suffix_ident_spec.
We shall now proceed to the definition of functions to update interfaces' path.

Function update_last_path_item (p:path) new_id : path :=
  match p with
    nil => nil
  | i :: nil => new_id :: nil
  | i :: r => i :: (update_last_path_item r new_id)
  end.

Function update_interfaces_path (li: list interface) new_id : list interface :=
  match li with
    nil => nil
  | (Interface i t p a c f ct cd) :: r =>
    (Interface i t (update_last_path_item p new_id) a c f ct cd) :: update_interfaces_path r new_id
  end.
Naturally, we need to prove that a list of interfaces remain well formed after applying update_interfaces_path.

Lemma updating_interfaces_is_well_formed:
  forall li id,
    well_formed_interfaces li ->
    well_formed_interfaces (update_interfaces_path li id).
Proof.
   induction li; intros; auto.
   simpl.
   destruct a.
   apply WellFormedInterfaces_Step with
     (i:=Interface i s (update_last_path_item p id) v r f c c0)
     (r:=update_interfaces_path li id); auto.
   Case "Unique Id x Acc".
     assert (well_formed_interfaces (update_interfaces_path li id)).
       apply IHli.
       inversion H; inversion H0; subst; auto.
     clear IHli.
     apply UniquePairs_Step with
       (int := Interface i s (update_last_path_item p id) v r f c c0)
       (r := update_interfaces_path li id); auto.
     SCase "First One is unique in the Tail of the List".
       simpl.
       inversion H. inversion H1.
       inversion H1; subst. clear H1.
       inversion H2; inversion H1; subst.
       clear H1.
       simpl in *.
       clear H2.
       induction r1; simpl; auto.
       destruct a.
       apply NotInPairStep with
         (int:=Interface i0 s0 (update_last_path_item p0 id) v0 r0 f0 c1 c2)
         (r:=update_interfaces_path r1 id); simpl; auto.
       clear -H.
       inversion H; inversion H0; subst. clear H0.
       inversion H1; inversion H0; subst; simpl in *. clear H0.
       inversion H3; inversion H0; subst; simpl in *; auto.
       apply IHr1; clear IHr1.
       SSCase "Premise 1/5".
         inversion H5; inversion H1; subst; auto.
       SSCase "Premise 2/5".
         inversion H3; inversion H1; subst; auto.
       SSCase "Premise 3/5". Focus.
         clear -H Case SCase SSCase.
         inversion H; inversion H0; subst. clear H H0.
         assert (unique_pairs (Interface i s p v r f c c0 :: r1)).
           clear -H1.
           inversion H1; inversion H; subst; simpl in *. clear H.
           apply UniquePairs_Step with
             (int:=Interface i s p v r f c c0) (r:=r1); simpl; auto.
           inversion H0; inversion H; subst; simpl in *; auto.
           inversion H2; inversion H; subst; auto.
         apply WellFormedInterfaces_Step with
           (i:=Interface i s p v r f c c0) (r:=r1); auto.
         inversion H2; inversion H0; subst; auto.
       SSCase "Premise 4/5".
         clear -H0.
         inversion H0; inversion H; subst; auto.
       SSCase "Premise 5/5".
         clear -H4.
         inversion H4; inversion H; subst; auto.
     SCase "Unique Pairs".
       inversion H0.
       SSCase "Interfaces are nil".
         rewrite H1; simpl.
         apply UniquePairs_Base; auto.
       SSCase "Interfaces are not nil".
         rewrite H1 in *; auto.
  Case "Well Formed Interfaces".
    apply IHli.
    inversion H; inversion H0; subst; auto.
Qed.
We can now proceed to the generation of components. Below, the generate_from_template function generates a list of n components from the component template given as parameter. It is not just about ensuring component id unicity, we must also consider the fact path in the interfaces must also be updated.
For the sake of simplicity, we shall consider it only copes with primitive components.
Function generate_from_template (template : component) (n : nat) {struct n} : list component :=
  match template, n with
     _ , 0 => nil
   | Component i p ic cl nil li nil, S m =>
        let li' := (update_interfaces_path li (suffix_ident i n)) in
        (Component (suffix_ident i n) p ic cl nil li' nil) ::
        (generate_from_template template m)
   | _, _ => nil
  end.

Lemma generate_from_template_spec:
  forall i p ic cl li n,
  forall l, l = generate_from_template (Component i p ic cl nil li nil) n ->
  forall c, In c l ->
  exists m, (c->id)%comp = (suffix_ident i m) /\ m <= n.
Proof.
  induction n; simpl; intros; subst.
  inversion H0.
  destruct H0; subst.
  Case "1/2".
    simpl.
    exists (S n). split; auto.
  Case "2/2".
  assert (exists m : nat, (c ->id)%comp = suffix_ident i m /\ m <= n).
    apply IHn with (l:=generate_from_template (Component i p ic cl nil li nil) n); auto.
  destruct H0 as (b, (H1, H2)).
  exists b.
  split; auto.
Qed.

Require Export Coq.Arith.Le.
Require Import Omega.
Lemma generation_has_unique_ids:
  forall i p ic cl li n l,
   generate_from_template (Component i p ic cl nil li nil) n = l ->
   unique_ids l.
Proof.
  induction n; simpl; intros; subst; auto.
  eapply Unique_Step; auto;simpl.
  clear IHn.

  apply same_nots'. intro; intros.
  destruct generate_from_template_spec with (i:=i) (p:=p) (cl:=cl) (ic:=ic)
                    (li:=li) (n:=n)
                    (l:=(generate_from_template (Component i p ic cl nil li nil) n))
                    (c:=e); auto.
  destruct H0.
  rewrite H0.
  assert (suffix_ident i x <> suffix_ident i (S n)).
    apply suffix_ident_spec with (n:=x) (m:=S n) (id:=i).
    omega.
  eauto.
Qed.

Lemma template_generation_produces_well_formed_components:
  forall c,
    well_formed_component c ->
    forall n, well_formed_components (generate_from_template c n).
Proof.
  induction n.
  Case "n is 0".
    destruct c; simpl; auto.
    destruct l; simpl; auto.
    destruct l1; simpl; auto.
  Case "n is not 0".
    simpl.
    destruct c.
    destruct l; auto.
    destruct l1; auto.
    split; intros.
    apply generation_has_unique_ids with
           (n:=S n) (i:=i) (p:=p) (ic:=i0)
           (cl:=c) (li:=l0); auto.
    destruct H0; subst.
    apply WellFormedComponent; simpl; intros; auto.
    fromfalse.
    apply updating_interfaces_is_well_formed.
    inversion H; auto.
    eapply well_formed_component_individuals; eauto.
Qed.