====== CR rapide du 16/04/09 ======
 
//(rédigé par PA)//

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

===== Travail à propos de la sémantique Kmelia =====

PS: Quelle est la prochaine analyse prévue ?

  * assemblage global
  * concurrence

===== Travail à propos de la traduction Kmelia2B =====



==== Fonctions ====

Comment déclarer des fonctions

  * mathématique

    non

  * fonction (fonctionnel)  --> voir [[types_fonctions#fonctions|fonctions en kmelia]]
    - prédéfinie **DEFAULT** 
    - use //maLibrairie// voir [[librairies|librairies kmelia]]

  * traduction en B des fonctions Kmelia :
    - soit via des lambda-fonctions B
    - soit via des opérations d'une machine incluses

  * syntaxe :
    * pas dans le modèle
    * dans la spec : mot-clé USE pour les [[librairies|librairies kmelia]]

  * modèle TODO
    * environnement (et bibliothèques de fonctions)
    * assemblage-type
    * composant-type

==== types et B ====

    * limitations : **POUR LE MOMENT** pas un problème
    * rester expressif sinon pas mieux que CSP+

==== postconditions ====

  * postconditions
  * result 
  * old(var)
  * tableaux
    * boucles : while (sucre pour le eLTS) //limitations possibles (ex: pas de com=
    * initialisation rapde à définir
    * fonction "prédéfinie"
    
==== initialisation ====

  * affectations simples



==== offert/requis ====

  * contexte virtuel et/ou contrainte de "même serveur" utile à l'assemblage
    * AL : même contexte virtuel
    * PA/GA : pas obligatoire, on préfère une contrainte en plus : plus souple virtuel = 
        * contexte = scope pour assertions
        * contrainte de même serveur peut se faire avec des contextes quelconques

   solution : uniquement des déclarations locales

version 1
   VirtualContext
      Variable
      Invariant

version2
      
   virtual Variable
   virtual Invariant

la 2 est choisie
  * pas de init
  * besoin de properties ? plus tard

  * requis : subrequires 
    * nécessaire ? lourd ?
 

==== contrainte d'assemblage ====

  * même serveur dans clause PROPERTIES

   _r1 = _r2
ou
   same_provider(r1, r2, ...)