Errata

These are the known errors as of 14 June 2023.

• Page 1, line 4 of 1.1 (this is embarrassing!): the period after "picture" should be a comma.
• Page 158, last line of last bullet point (end of 8.8): "... may refer to Goal, System and Environment classes". ("System" was missing).
• Page 149, in the second clause of the class invariant, replace is_evaluated by is_investigated. (For more clarity, the postcondition of set_reserve could include a comment similar to the one for the previous routine, stating that is_investigated still holds thanks to that invariant clause.)