**CR REU du Vendredi 29 mai** 
{{tag> kmelia cr B }}
-----------------------
Facs09 - CA, AL

Suite des experimentations en B (sur l'exemple Stock...)

Après examen des obligation de preuve non déchargées, on s'aperçoit que
la post-cond (de l'exemple) est incomplete ;
- par exemple, on a dit dans l'Inv : que tout elt de cataloque a P(elt) en l'occurrence 0<elt<Borne ;
dans la poste on a omis de dire que les elts ajoutés à catalogue ont P.
- dans la poste on n'avait pas décrit comment étaient les éléments du (new)catalogue ;
en gros il faut considerer tous les intervales (compléments de ]0,Borne] )

A partir de ces constats, on modifie la spec Kmelia, on retraduit en B, on tente de verifier ;
la preuve resiste encore ;
on analyse les obligations de preuve, et l'etat de notre spec ;
(Soit Not NonErreur et Bonne propriété du résultat)
(Soit Erreur et Rien n'a changé dans notre nouvel etat)  ** à ajouter ;

Encore insuffisant ;
Pistes à explorer pour corriger la spec Kmelia :
 - renommer/distinguer proprement les  bornes : MaxRef, StockSize, etc
 - lever la confusion entre NullInt et "Error", etc, ne pas utiliset la meme NullInt pour plusieurs choses...

Remarque :
Preciser explicitement pour (la semantique de) Kmelia que, lors  des transitions, tout ce qui n'a pas été modifié, reste inchangé ; ==> ainsi on peut en trenir compte dans les traductions. 
------------------------