====== CR rapide du 12/02/09 ======
 
//(rédigé par PA)//

Présents : PA, CA, GA, MM, PS

===== Kmelia =====





==== discussions sur la grammaire Data ====

=== Effets de sur la dynamique ===

== actions ==

 inclusion des expressions

== nommage des canaux ==

possibilité de factoriser

     * appel de service : pas de factorisation
 
    channel[:<RoleId>}[<selector>](!|?|!!|??)message(param*)}
    selector : '['i|:i|ALL']'

     * sous-services opt :

   channel[:<RoleId>}[<selector>] {servName1, servName2, ...}

     * sous-services mandatory: pas de factorisation : un seul par transition   

=== Rappel des clauses ===

  pre/post 

   * obs/non-obs
   * listes de prédicats nommés

  contexte virtuel + nommage des variables présumées

=== Propriétés attendues ===

== Composant tout seul ==

  - tous les offerts sont corrects
      * Pre / Post de l'offert préserve Invariant
      * Sous-Services : enchaînements corrects de Pre / Post
        * protocoles
        * eLTS restreint à opt/mandatory (subprovides)
      * Pre + eLST => Post : étude de l'effet des actions
  - tous les requis sont corrects
      * Pre / Post du requis cohérent dans le contexte d'appel du service offert appelant
  - Invariant ?
  - Obs/nObs : discussion sur incohérence entre les deux => lever des erreurs de spécification. Ex: Obs correct mais nObs non correct -- sans doute plus facile de vérifier uniquement Obs

Règles

  * 1.a assertions

   Invt + Pre + Post => Invt

  * 1.b enchaînements de deux services 1 et 2

   Invt + Pre1 + Post1 => pre2 & Invt

  * 1.c actions

   Invt + Pre + Actions => post & Invt

  * 2 Pour chaque appel d'un requis Sr on a la cohérence des "assertions" (état du service sous forme de prédicat Pei)

   Pei |- pre(Sr) 
   post(Sr) + Pei |- Pej 

  * 3 Invariant et initialisation

   Invt <> false
   Init => Invt

== Assemblage ==

  * voir les travaux discutés précédemment

== Composition ==

===== Coloss =====