For convenience, we will refer to each change using the number of the page on which it appears. Detailed explanations are given below.
in should be
:, proof has spurious assumption.
P
|- should
be =>
In the final proof tree on the page, the step labelled
\/-intro2 should be labelled \/-intro1, and
vice versa.
In the sketch proof at the bottom of the page, p and q are reversed in the antecedent and a and b are reversed in the justification.
In the proof at the top of the page, the `element of' symbol is used in a declaration; a colon should be used instead. Worse still, there is an instance of p in the assumption that simply shouldn't be there. It has been removed.
The proof at the bottom of the page is made easier if the
just-introduced compre-s rule is employed instead of the
standard compre. In the revised version, the subsidiary
proof on Page 65 is no longer necessary.
On page 66, last paragraph of Section 5.3, it states that the
definition of F is given in Chapter 10, whereas it
actually appears in Chapter 8.
Half way down the page, the sentence that begins `the ordered pair (a,b)' should begin `the ordered pair (x,y)'.
Although not an essential part of the explanation, this is possibly the most embarrassing error in the book; the answer to the multiplication should be 324, not 234.
In Example 5.21, the result of the first set difference should be {1} and not {6}.
The declaration of basic types in Example 6.1 should be [Guest,Room], to be consistent with the text that follows.
There is a missing powerset symbol in the definition of safe: it should be a set of sets of people.
The sentence that begins `We may compose...' should read as follows: `We may compose the relations drives and uses to find out which fuels a driver may purchase.
Example 8.5 used a function called approx, whose definition was sufficiently complicated as to obscure the point of the example, which is intended to illustrate the use of the lambda notation. This has now been replaced with an alternative example.
At the end of Example 10.2, we stated that status d is
well-defined; we meant to say that status~ d is
well-defined.
The account of bindings and decoration is not particularly helpful.
A far, far better way of doing things is to explain decoration of
bindings; theta Schema ' is a decorated form of
theta Schema, and is an object of the same schema type
Schema. The two bindings can therefore be equated; they
are equal if and only if the value of each variable is equal to the
value of its primed equivalent: see the on-line version of the
text for further details.
There is a missing existential quantifier in the predicate part of
the StartBooking schema, leaving the variables in the binding
of BoxOfficeInit' unbound. The predicate part should begin
with the quantification \exists BoxOfficeInit. It would
also be clearer if the binding of BoxOfficeInit' were replaced
with one of BoxOffice', which was the original intention.
In the last piece of displayed mathematics on the page, there is a semicolon where a dot ought to be. The proof that the promotion is free is unnecessarily complicated, overlong, and - at one point - actually incorrect. This proof, and the rules that precede it, have now been replaced.
There is a missing existential quantifier in the predicate part of
the Create0 schema, leaving the variables in the binding of
FileInit' unbound. The predicate part should begin with the
quantification \exists FileInit. It would also be
clearer if the binding theta FileInit' were replaced with one
of File'.
In the last paragraph of the page, the first sentence should read `are relations of' rather than `of relations of'.
The predicate (a universal quantification) at the top of the page includes a declaration of is' and os', neither of which are required in the body of the predicate.
The words `strictly positive' in the first paragraph should be replaced by `non-zero', to match the displayed mathematics.
All of the quantified expressions apart from the first (describing the initialisation) are missing p? from their declaration parts. This variable should be universally quantified: the conditions should apply for all values of the input p?.
In two places on this page, InitCMemory should be written as CMemoryInit (to be consistent with the name of the abstract initialisation).
All of the quantified expressions apart from the first (describing the initialisation) are missing n? and m! from their declaration parts. The first of these variables should be universally quantified, the second should be existentially quantified.
There is a piece of information missing from the state of the Apollo booking system: the separated ticket must not be one of those in the pool (this is an invariant of the system, but needs to be made explicit if the proof is to be completed)
tkt \neq null \implies ticket\inv tkt \notin apool.
In the last piece of displayed mathematics on the page, there is a
turnstile |- that would be better understood as an
implication symbol =>.
In the first sentence on this page, the noun `others' should be singular. On the same page, the type Digit is declared with an additional s at the end of its name.
The sentence immediately above the schema is missing the word `by' following `described'.
The sentence that begins `Notice that these are easier to apply that those given' should read` Notice that these are easier to apply than those given'.
The word Systems has been mis-spelt twice in the displayed mathematics (as Sytems).
The repetition of `that' in the second paragraph is not intentional. Also, in the last paragraph on the page, as a should read is a.
The sentence in the middle of the page should read Any variable that is not assigned to will have the same value after the operation as before....
The free variables in the predicate part of the schema SectionInit should all be primed to match the decoration. Further, the value of ins' in the definition of STransmit is wrong; it should be changed to match that of rec'. See the new version of the page.
In the first sentence, the word `our' appears for no good reason. In the lower half of the page, the schema RetrieveExtSection should not be decorated in the three predicates that involve preconditions (this should be obvious from the declaration).
The identifier s on the fourth line of the displayed mathematics should be ins.
| text | slides | exercises | solutions | cards | contents |