page 75

The last sentence on the page should be changed from:

Thus, the month can be extracted from a date by selecting field 2:

to:

Thus, the street can be extracted from an address by selecting field 2:

page 90

There is a problem with the definition of the Sample function definition. It makes use of the Sex function. However, Sex takes a CPRNo`Digits4 as a parameter whereas in Sample it is being passed a CPRNo in the line:

p in set pop and Sex(p) = sexreqd

One solution is to make use of the GetCode() operation that is defined on p93.

The line then becomes:

p in set pop and Sex(p.GetCode()) = sexreqd

This change applies to both boxed definitions of Sample.

page 93

The second sentence following the first VDM++ box should have:

(introduced later)

changed to:

(introduced previously)

page 155

The body of CarPassingEvent should say:

NewPassage(distanceBetweenLoops / drivingTime)

instead of:

NewPassage(distanceBetweenLoops * drivingTime)

page 162

The definition of ResetLog and WriteLog should be changed to:

---

class OperatorControl

...

public ResetLog:() ==> ()
ResetLog() ==
  atomic
   ( messageLog := [];
     locations := [] );

public WriteLog: seq1 of char * CWS`Location ==> ()
WriteLog(message, location) ==
  atomic
  ( messageLog := messageLog ^ [message ^ ConvertNum2String(location)];
    locations := locations ^ [location] );

end OperatorControl

---

This change is necessary in order to ensure that the invariant (requiring the length of the instance variables messageLog and locations to be equal) is checked after both instance variables are updated.

page 180

The first box should be changed to:

---

class CongestionSensor

...

instance variables
  passageSensors: map CWS`Lane to PassageSensor := {|->};

end CongestionSensor

---

page 292

Figure 12.3 should be changed to the following figure:

page 355/356

Exercise 5.1 All three boxed solutions should be modified as described for p90 above.

page 357

In the solution to Exercise 6.7 should the answer for the first exercise only one quote with apple.

page 362

In the solution to Exercise 7.8 should the answer for the second exercise be changed from [9,3,2,3] to [true,false,false].

page 364

In the solution to Exercise 7.12 should the answer for the first exercise be changed from [true,false,4] to [true,true,4].

page 365

In the solution to Exercise 7.16 should the answer to the last exercise be changed from {[5]} to {[5,4,5]}. In the solution to Exercise 8.2 should the answer to the last exercise be changed from {1 |-> 0.5} be changed to {|->}.

page 366

In the solution to Exercise 8.6 should the answer to the last exercise be changed from {1 |-> 5, 3 |-> 1, 5 |-> 1} be changed to {1 |-> 6, 3 |-> 1, 5 |-> 1}.