CR REU du Vendredi 29 mai
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 :