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 =>
Articles
