lundi 19 janvier 2015

Errata de "Spécification formelle avec B" H. Habrias, Hermès éditeur

Spécification formelle avec B

Errata et compléments, précisions etc.
____________________________________________________________
H. Habrias version n° 2 du 24-09-2002

Table des matières

Changer "Chapitre 1, Les services de B" pas "Les sources de B" comme l'indique le titre du dit chapitre.
page 76
supprimer un des textes de note de bas de page
page 53
Si nous voulons que l'Atelier B génère le code C, il faut que l'opération boucle de la MACHINE MainLoop soit nommée main et non
boucle. On fera attention à ne pas confondre la "main" (hand) avec le "main" (principal) !
page 135
Figure 6.6, supprimer b5 de l'ensemble d'arrivée B
page 137
Figure 6.8, supprimer b2 de l'ensemble d'arrivée B
Figure 6.9, supprimer a1, a4, a5 de l'ensemble de départ A
page 141
Figure 6.15, supprimer la flèche allant de a3 vers b2
page 143
Figure 6.17, supprimer a4 et a5 de l'ensemble de départ A
page 145
Figure 6.20, supprimer b2 de l'ensemble d'arrivée B
Page 153
Chapitre 6
6.3.5.2.1.
La factorielle est exprimée sous la forme :
Mettre n devant le premier signe d'appartenance
Page 161
6.3.10.
prj2(E1, E2) = {(1,v)  au lieu de prj2(E1, E2) = {1,v)
Page 163, 8ième ligne
En VDM (voir chapitre 17)
Page 164, note de bas de page
Voir chapitre 15
page 198
dans la machine Iut2 on doit spécifier l'invariant sur les phases avec un OU sinon (phase = 1 ET phase = 2) = false !
Dans la précondition de inscription c'est phase = 1  (et non pas 0) qui doit être lu.
page 199 :
 pour l'initialisation l PO est évidemment :
[subst. init] Invariant
Page 206
Chapitre 9
7ième ligne
La terminaison (au lieu de la faisabilité)
Page 211
13ième ligne
remplacer par non trm(S) => fis (S)
page 214
L'exemple de la substitution WHILE est erroné.
page 232
Chapitre 10
10.1.1.2.
Dans l'invariant (ligne 13), remplacer aPourAuteur1 par aPourAuteur2
page 242
Notre exemple d'un automate avec des sorties qui sont des actions n'est pas utilisable dans le cas où les actions seraient des opérations
paramétrées.
Page 248
Chapitre 11
Ligne 19
CoursOuverts est défini comme le ran(estInscritA)
ÉtudiantsInscrits est défini comme dom (estInscritA)
Page 256
Ligne 1
Pour passer de l'état E1 à l'état E3 (au lieu de E2)
Ligne 22 dans l'encadré
Remplacer coursOuverts := coursOuverts - {coursD} par
coursOuverts := coursOuverts - {cours0}
Page 270
Chapitre 12
Encadré de droite
Ajouter la clause INVARIANT
xx = yy
page 250
Nous avons écrit en 11.2.2.
" En B classique, on ne le peut pas." En fait, on peut mais c'est plutôt "lourd" à exprimer... ce qui fait qu'on risque ne pas y penser. Disons
que "ce n'est pas naturel en B classique".
page 270
Machine MAbstraite
supprimer le v en bout de linge xx:= xx + 1
page 273
Il manque l'initialisation pour le REFINEMENT
page 275
MACHINE MAbstraite3
changer Vv par vv
Page 287
Chapitre 13
Ligne au dessous des encadrés
(voir Chapitre 12)
page 352
Chapitre 16
16.1.2.1.
Remplacer la flèche en trait noir épais par le symbole de la garde ==>
Page 354
16.2.1.2
Entrée sur le continent, remplacer n := n + 1 par n := n - 1
16.2.3
5ième ligne
(en nombre n) à remplacer par (en nombre a)
Page 373 et suivantes
Chapitre 18
A Abstraction fonctionnelle
Remplacer le l dans les formules par la lettre grecque lambda
Page 383
Chapitre 18
Expressions mal définies
9ième ligne
remplacer le e de xx e dom(ff) par le symbole mathématique d'appartenance ensembliste.
Page 392
Priorité des opérateurs
6ième ligne

remplacer fi par => 

Aucun commentaire:

 
Site Meter