Known Errata of Volume 1

Some known errata are given here for reference.

I recommend the following format and style for typos (J. Xiang):

p.xx, l.yy: ..."typos"... --> ..."corrections"...[?] (XYZ)

(p. : page; xx: page number; l.: line; yy: line number; "typos": the bugs or mistakes; "corrections": the corrections; ...: the words or sentences before or after the "typos"/"corrections"; (XYZ): your initials)

In case you are not confident with the correction, then a optional ? ([] denotes Optionality) can be added at the end of record.

All the typos should be ordered by the page and line numbers, i.e., p.xx, l.yy, such that others can easily find the place and insert new records. In this case, I think the number of record is uncessary.

---------------------------------------------------------------------------------------

p.VI, left column poem, l.1: "footseps" --> "footsteps" (Dines Bjorner)

P18. The last sentence of the 4th paragraph, "Michael Jacson [308]
refers to domain descriptions as imperative." Here "domain
descriptions" should be "software design". (Liu Bochao)

P26. The 3rd sentence of the first paragraph of section 1.4.3, "As
for all crafts,....,different size planners, ...". Here "planners" should be "planers". (Liu Bochao)

P95. In item (5), "We express by:\lambda x.\lambda y.\lambda
x. E(x,y,...,z)". Here the third binding variable "\lambda x" should
be "\lambda z". (Liu Bochao)

P101. In the example given just in the 2nd paragraph, type "D"
should be declared. (Liu Bochao)

P101. A typo at the footnote, "evauation" should be "evaluation". (Liu Bochao)

P103. In the example given in the second paragraph,
" ...........
And, instead of expression function application as :
f(a)(b)(c)". Here "expression" should be "expressing". (Liu Bochao)

P110. Section 7.1
"x, \lambda y.e, f(a)
........... We "read" the expression \lambda y.e as follows: The
function of x ..... all free occurrences of the variable x with
\lambda-expression a". Here the last two "x"s should be "y". (Liu Bochao)

P125. The 4th line,
"3. <\phi_0,\phi_1,....,\phi_{n-1}> F^n T> = \phi_{n-1}". Here "F^n"
should be "F^{n-1}". (Liu Bochao)

p.130, l.20: "largest" common multiple --> "lowest" (LI XIN)

p.137, l.-2: really ought to "so" so --> "do" (LI XIN)

p.207, l.11: The "natural numbers" are ... --> The "integers" are ... (Xiang Jianwen)

p.207, l.12: -2,"-2",0,1,2 --> -2, "-1",0,1,2

p.208, l.-10: or $t \neq t'$ (and "$\not\equiv"$) --> or $t \neq t'$ (and "$t \not\equiv t'$") (Xiang Jianwen)

p.209, l.17: there are only and exactly "the three" enumerated values --> there are only and exactly "n" values (Xiang Jianwen)

p.218, Exercise 10.4, l.-12: From "credit cards" one can observe " " customer name, a credit card number, and, hidden from view, "the" number of a credit card account -->
From "a credit card" one can observe "a" customer name, a credit card number, and, hidden from view, "a" number of a credit card account ? (Xiang Jianwen)

p.232, l.17~18: For an early example of what such "rewrites" mean, see Example 16.10. --> The whole sentence should be footnote rather than text? (Xiang Jianwen)

p.232, l.-7: each model is an algebra, a set of named values and a set of named operations on these. --> each model is an algebra, "i.e.," a set of named values and ... (Xiang Jianwen)

p.233, l.1~2: some part of a reality, or of a constructed such, or of requirements to, or of actual software. --> some part of a reality, or of a constructed such "a reality", or of requirements to "the reality", or of actual software. ? (Xiang Jianwen)

p.233, l.9: The model is not what it models, only a model of "it"! --> The model is not what it models, only a model of "what it models"!? (Xiang Jianwen)

p.246, l.16: Examples 12.3 and "and" 12.4 --> Example 12.3 and 12.4 (Xiang Jianwen)

p. 246, l.25: Example 12.3 and "and" 12.4's --> Example 12.3 and 12.4 (Xiang Jianwen)

p. 249, l.2: Example 12.3 and "and" 12.4's --> Example 12.3 and 12.4 (Xiang Jianwen)

p.253, l.5: By "looseness of a specification" we mean a specification which features elements of underspecification or nondeterminism. --> By a loose specification we mean a specification which .... (Xiang Jianwen)

p.328, Example 15.3, the second line "...and let ns be a set of values of type A" -->" ns" should be "sas", as it is defined in the example. (Guoqiang Li)

p.329, Also in Example 15.3, a line before the definition of ''merge:'', there exists a intersection, "elem p(i) \intersection elem p(i+1)" --> "elem p(i) \intersection elem p(i+1)=\emptyset". (Guoqiang Li)

p.433, In the first graph some definitions occur like"By argument_pattern we mean....", and "result_patterm is a pattern with...", however, in the above example, there are no such denotations, similar definitions are "arg_pattern", "res_pattern", respectively, it should be uniformed. (Guoqiang Li)

P434. the 5th line of the first paragraph. "the cases expr of expression" where "cases" should be "case". (Liu Bochao)

P.435, the sixth line after 19.2.1 in the expression $\lambda a. \mathcal{E}_b(a)$, two $a$ should be uniformed. (Guoqiang Li)

p.450, Example 19.10 "case vs of {} -> chaos v \cup vs' -> mk_Sty(xty(v)) end" The comma is missing between "chaos" and "v". (Liu Bochao)

p.451, Example 19.11 "wfBind : Bind' \times VAL -> Bool" It should be "wfBind:Bind' -> Bool".(Liu Bochao)

p.451, Example 19.11 wfBind(mk_ccs(cs,_),mk_SeV(vs)) =
.................
\forall i:Nat . i \in inds cl => wfBind(cl(i), bl(bi(i))) end
In the last line of this case of the function wfBind definition, "bl" and "bi" has never been defined yet. It should be "vl(im(i))". (Liu Bochao)

p.453,Example 19.12,Bind(mk_ccs(cs,on),mk_SeV(vs)) =
let
................
=> wfBind(cl(i),bl(bi(i))) in
...........
The same as the previous one. (Liu Bochao)


p.470. footnote. "Simmilar for the use of the I name elow and b[3]" --> "Simmilar for the use of the I name below and [3]".(Liu Bochao)

p.475. The last line " Nm, Tn, 1Loc" where "Tn" should be "Vn".(Liu Bochao)

P.476. The 6th line "SVAL == mkintv(i:Int)mkboolv(b:Bool)LOCV", where "LOCV" should be "LVal". (Liu Bochao)

P.476. The fourth line of "type" declaration for "Location and Value Types", "RType == mkrect(rt:(Rn->1Typ))" with "m" underlying "->", where "Rn" should "Nm". (Liu Bochao)

p.478. The 4th and 6th line of the code just above "Semantics" section. "Sel::v:Vn rn:Rn" where "Rn" should be "Nm"; "Fld==null mkRn(rn:Rn)" where "rn:Rn" should be "rn:Nm".(Liu Bochao)

p.476. The second line to the bottom, "...r:Rn. r\in dom rv..." where "Rn" should be "Nm".(Liu Bochao)

p.481 The last sentence of the paragraph just before Section 20.4.3. "The signature of incr defines that incr applies to a value of type Unit .....", where both "incr" should be "get".(Liu Bochao)

p.484 The third line "These are P(a), e_1, e_2,...e_n, ll(a), ........" where "ll(a)" should be "lst". The 4th example given here "" should be ">". (Liu Bochao)

p497. The 7th line after "Simple Interpretation Functions". "E:almost as defined above, but without dynamic tests" should be "E:almost as defined as above, but without dynamically testing that v is in \rho" (Liu Bochao)

p.499. The fourth line in the second "Techniques" paragraph for "Applicative States". "... a map of state components to (state) component associations...." where "a map of state components" should be "a map of state component names" (Liu Bochao)

p.511 Characterisation. By concurrent
specification programming ..... between actions of proceses
(* proceses is mispelled *) can be left unspecified ..... (Liu Bochao)

p.534 Compound Events. In the first equation, "a.3 -> P7" where "7" should be
eleminated. (Liu Bochao)

p.535 Section Input and Output. The second equation: "d! k:K -> Q(k) = [] k: K . d .k -> P(k)" where "P(k)" should be "Q(k)". (Liu Bochao)

P584. The fourth line "See Vol. 1, Chap. 7 , Sect. 7.7.4.3." Here "Sect. 7.7.4.3" should be "Sect. 7.4.3". (Liu Bochao)

P589 "208. Dependability requirements: .... or robustness
requirements,...or robustness requirements.", where there is a duplication here, "or robustness requirements" should be deleted. (Liu Bochao)

P629. "585. Reliability:......( ... . As such, accessibility is (to be ) expressed in a machine requirments document.)", were "accessiblity" should be "reliability". (Liu Bochao)

p630. "600. Requirements prescription unit: .... (Usually prescription prescription units ....)"
were "prescription prescription units" should be "requirements prescription units". (Liu Bochao)

p632. "625. Satisfiable: A predicate is said to be satisfied ....", were "satisfied" should be "satisfiable". (Liu Bochao)

p.637. "676. Stage : (1) ...., or which starts from a complete phase
documentation of kind stage, and results in a complete phase
documentation of another stage kind ...." , where the first "kind stage" should be "stage kind". (Liu Bochao)

p.638 "685. Step: ... from a more abstract to a more concrete description.", where "description" should be "description (or prescription, or specification)". (Liu Bochao)

p.638 "688. Store: Same as store ...." , where "same as store" should be "same as storage".

p.646 The third line, "...(i--ii) if the shared ....", where "(i--ii)" should be "(i)". (Liu Bochao)

p.646 "Value:....past participle of Latin valEre to be worth, be strong.....", where "be worth" should be "be of worth". (Liu Bochao)

p.647 "Vertex :Same as an edge", where "edge" should be "node". (Liu Bochao)

posted by Liu Bochao @ 12:16 AM