1. (p7) Semantic definition of free variable). There is a missing "not",
where in the third last paragraph it should read 
   "x is not free in p if p is invariant under changing x"
[Thanks Steve Brookes.]


2. (p8) The ok post for nondet assignment should be \exists x.p and not
\exists x'.p 

3. (p21) "Next, the assert rule plus"
|-> "Next, the assume and error rules plus"

The phrasing is a leftover from an earlier version which used
"assert x != 2,000,000" in the code rather than "if..error()".

4. (p21) line -4: replacing x |-> replacing z

5. (p25)
The effect of this could be seen if we replaced the statement assert(x==4) by
assert(x==5) and
simultaneously the flaky achieves [ok: x is odd] with [ok:true].
|->
The effect of this could be seen if we replaced the statement assert(x==4) by
assert(x==5), the statement x=3 by "assume (x is odd)", and
simultaneously the flaky achieves [ok: x is odd] with [ok:true].

[Thanks Aindya Banerjee for 2-5]