(rédigé par PA)

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

• nouvelle version notes PS 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

    Pres and Invtc(before) and Posts ⇒ Invtc

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

rapport MM en cours ici

discussions sur la confusion type/valeur, type/ensemble

correction de quelques types

…

plus tard

retrouver la dernière discussion sur le sujet