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

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

===== Kmelia =====

==== discussions sur la sémantique de Kmelia ====

  * nouvelle version notes PS {{kmelia:simplest_v2.pdf|ici}}

  * init: service ou pas : NON\\
    peut évoluer avec les composites

  * init var valeur par défaut
    * AL: c'est mieux d'expliciter
    * valeur par défaut pour chaque type de donnée (cf ancienne version Kmelia) : NON
    * obtenir une valeur quelconque de l'espace d'état
    * pb des types utilisateurs
    * __choix__ : ??
  * qu'est-ce que la sémantique ? abstraction des valeurs
    * sémantique dénotationnelle
    * ici c'est de l'opérationnel 

   [b = a+1] action
   si [|e|]e(V) alors [|a|] sinon skip;

  * test garde toujours vraie / faussse : "c'est l'analyse et pas la sémantique"\\
état inaccessible
  * trois niveaux
    * syntaxe
    * sémantique (abstraire détails)
    * analyse 

  * retour pre/post
    * pre/post service mais pas d'invariant

    Pre_s and Invt_c(before) and Post_s => Invt_c

en B

    Pre_s and Invt_c => [(Post_s)B] Invt_c

    * eLTS(pre) => Post

en B (post confondue avec Invt)

   [eLTS] (pre and Invt) => Post
   Pre_s and Invt_c => [(eLTS)B] Invt_c

   * raffinement

    Pre_s and Invt_c(before) => Pre_s and [(eLTS)B] NOT [(Post_s)B] NOT Invt_c

    A[=R en B (pb inclusion)

  * pb du prouveur : utiliser B dans le bon sens (voir Coq, PVS)
    modifier INVT est une solution mais PB de traçabilité\\
deux solutions :
     * une propriété à vérifier : comment en B
     * preuve en B : quelle propriété Kml est vérifiée ?
         travailler sur implication et non équivalence


==== discussions sur Kmelia/B et vérification ====

rapport MM en cours {{kmelia:rr_xx_yy.ps|ici}}

discussions sur la confusion type/valeur, type/ensemble

correction de quelques types

...

==== discussions sur shared services et vérification ====

plus tard
  retrouver la dernière discussion sur le sujet