====== CR rapide du 01/04/09 ======
 
//(rédigé par AL, mis en ligne par PA)//

Présents : CA, MM, AL

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

1) il ne nous semble pas intéressant dans un premier temps de ce focaliser sur la traduction des types non supportés "nativement" par B.

* array
* struct
* String

Il vaut mieux ce concentrer sur des problèmes plus "scientifiques" : traduction des posts, implémentation


2) rédaction du document de synthèse Kml2B de MM : plutôt que séparer les explications par rapport au type, puis les variables faire pour chaque type, déclaration du type, d'une variable de ce type, de l'initialisation de la variable, de l'utilisation de la variable, etc.

3) MM devrait nous faire une présentation "détaillée" des travaux de Ledong à propos de la traduction Postcondition OCL -> B

----
fixer une date prochainement pour cette présentation  : dans 15 jours ?
----

//+ MM indique ne pas avoir trouver d'autre etat de l'art à ce propos, où plus globalement à propos du lien entre Postcondition <-> affectation/substitution//

Cela est étonnant.


4) discussion avec MM sur la traduction de la post avec des valeurs avant/après, et qq constructions plus complexes que uniquement =

  (voir les détails précis dans le cahier de MM)

----
reflexion à avoir autour le la notation Kmelia dans la Post ?
Actuellement choix fait de noter la variable avant pre(toto) et toto la variable après.
----

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

6) que devient l'interface d'un composant ? d'un service ?

7) le problème de la traduction Kmelia2B du eLTS ?
dans le cas de eLTS "arbre", trouver tous les chemins, et avec un
CHOICE .... OR ... OR .... END séquentialiser en B tous ces chemins.

Il n'est pas si aberrant  que cela de faire l'hypothèse de eLTS sans cycle.