For convenience, we will refer to each change using the number of the page on which it appears. Detailed explanations are given below.
<| should be
|>
The phrase `we not...' should read `we are not...'.
The left-hand antecedent for the forall-introduction step should in fact be the left-hand antecedent for the exists-introduction step.
In Example 4.12, the term part of the quantification should state that p is not equal to q.
Example 4.16 should read:
The statement that Marie Curie is the person who discovered radium could be formalised asMarie Curie = u y : Person | y discovered radiumProvided thatE_1 x : Person @ x discovered radiumwe may then inferMarie Curie in Person /\ Marie Curie discovered radium
The proof step justified by [dec-mem] should be justified by [/\-elim1].
There is an extra condition stating that x should be an element of s in the antecedents of the first rule labelled compre-s. This rule should be the converse of the other rule with the same label, presented immediately below.
Also, the fork in the proof tree at the bottom of the page should be justified by implies-elimination, not forall-elimination.
In the proof on this page, there is a step justified by [dec-mem]. It would be easier to follow if the assumption were a conjunction, and the rule was [/\-elim1].
There is an extra equality symbol in the statement
P_1 {0,1} = {{0},{1},{0,1}}
making it into an abbreviation definition, when it should be a simple
assertion.
The left-hand branch of the proof at the top of the page is not necessary. The compre-s rule allows us to deduce false from the statement that n is an element of the empty set of natural numbers.
The final line of the proof at the bottom of the page is justified by the rule `one-point-s'. This should read simply `one-point', as it is justified by the one-point rule for existential quantification introduced in Chapter 4.
There is a maplet missing from the equality involving direct^3: the pair (singapore,perth) should also be present.
The function pair should take a natural number n, not a natural number x to be consistent with the statement given in the mathematics.
There is a blank line in the second paragraph that should read `the set'.
The domain restriction symbol in the informal definition of
filtering should be a range restriction (the expression s <|
A is not even well-typed). The definition should read
s |` A = squash (s |> A)This error is repeated in the formal definition further down the same page.
The sentence that begins `The step marked P t' should read `The step marked P r'.
The justification `P r' in the equational reasoning proof has a roman `P' and a roman `r': these should be italicised.
The element zero in the lower part of the axiomatic definition is missing a pair of set braces.
The element zero in the lower part of the axiomatic definition is missing a pair of set braces.
There is a missing angle bracket in the data expression at the bottom of the page: it should have the following structure:
(1, < (2, <>), (3, <>), (4, <(2, <>)>) >)
The inference rule given at the end of the sentence beginning `This type has a single constant...' would be more easily recognised if the two remaining instances of T were replaced with nat.
The third line of the proof at the bottom of the page is wrong: the
flip function is missing from t1 and
t2. A correct proof would read as follows:
(flip ; flatten) branch (t1,t2) = flatten (flip branch (t1,t2)) [defn of ;] = flatten (branch (flip t2, flip t1)) [defn of flip] = flatten (flip t2) ^ flatten (flip t1) [defn of flatten] = (flip ; flatten) t2 ^ (flip ; flatten) t1 [defn of ;] = (flatten ; reverse) t2 ^ (flatten ; reverse) t1 [P t1 /\ P t2] = reverse (flatten t2) ^ reverse (flatten t1) [defn of ;] = reverse (flatten t1 ^ flatten t2) [property of reverse] = reverse (flatten branch(t1, t2)) [defn of flatten] = (flatten ; reverse) branch(t1, t2) [defn of ;]
The declaration of sold is perhaps misleading. In the
sentence that begins `This relationship' we are making a statement
about sold: the set membership symbol (epsilon) would be
more appropriate than the colon here.
There is a missing line in the deductive proof at the top of the page. The deduction
P t1 /\ P t2 => P (branch (t1,t2))should appear before being generalised with the forall-introduction rule.
The identifier `sep' should be in sans-serif, rather than italics, to remind the reader that it is a constant of a free type.
The sentence that begins `For example' has a missing preposition: it should read `... we may write s.a and s.c to denote...'.
As a matter of style, it would be better if the order of the two conjuncts in the set comprehension half-way down the page matched the order of the same two conjuncts in the schema definition.
On the fifth line from the bottom: `the a components' should read `the a component'.
On the first line: `information that' should read `information than'.
The identifier `sep' should be in sans-serif, rather than italics, to remind the reader that it is a constant of a free type (same error as Page 152).
The sentence `If we wish use the same structure' should read `If we wish to use the same structure'.
The phrase `may obtained by existentially quantifying' should read `may be obtained by existentially quantifying'.
The binding of s in the equation for score' is written using a `maps to' symbol rather than a `binds to' symbol (three times). Also, as a matter of style, it would be better to have removed the s' from the declaration part of third quantification; it is no longer required.
The type Person in the schema named MailSystem should be User, to match the following schemas.
The paragraph that begins `Figure 13.2' is misleading. It should read:
Figure 13.2 shows a mail system with three users: Carolyn, Denise, and Edward. Each user has a personal mailbox with an appropriate address. Carolyn and Denise share ownership of the system administrator's mailbox, with address admin. Edward has two mail addresses, and hence two mailboxes: edward and edwardc.
The diagram (Figure 13.2) would be more helpful if edward and edwardc were associated with different bindings of type Mailbox. Of course, these elements can be associated with the same binding, but this is unlikely to happen in practice.
The last article on the first line of Section 13.2 should not be 'a' but 'an'.
The second line from the top of the page refers to the schema GlobalPurchase. This name should be subscripted with a zero, as it is later on the same page
.The statement of the universal one-point rule is a copy of the existential rule, when it should read thus:
forall S @ theta S = t => P =========================== t in S => P[t/theta S]
The side condition remains the same.
The last line of the third proposition on the page would be more easily understood if the instances of schema name Data were decorated with primes.
The first sentence has a superfluous occurrence of the word `which' in it.
At the bottom of the page, the word emptyset appears
in place of the empty set symbol. Also, the preceding sentence should
begin with the word `Once' rather than `One'.
In the proof step justified by `one point rule, twice' the first spot should be a vertical bar, and the second should be a conjunction symbol. There is also a missing parenthesis on the same line.
The last schema on the page is not the schema it claims to be. A moment's inspection should convince you that it is, in fact, the precondition of Promote, mentioned in the previous sentence. The precondition of AssignIndex is
+--------------------------------- | Array | new? : N | index? : N +--------------- | index? \in dom array +---------------------------------There is also an unwanted prime in the schema quantification for `pre AssignIndex.
The instantiations of Local and Global on the third line of the proof didn't happen. The names should be changed to match the previous line.
The maplet s? |-> c? appears reversed twice in the
table of preconditions.
The ninth line from the top: `keys with data' should read `keys and data'.
There is a missing Xi symbol in the schema definition of KeyError. The declaration part of the schema should insist that the after-state is the same as the before-state.
The eighteenth line from the top: `is a basic type' should read `as a basic type'.
In the first paragraph of Section 15.5, the sentence containing 'should we able to' has been changed to `can we destroy an open file?' which is grammatically correct and makes more sense.
We imply that the initialisation theorem for the data type File is required if you wish to show that the requirements upon the file system are consistent. In fact, this is not the case: you can initialise the file system even if files themselves are impossible entities.
In the first schema on this page, the message `file is not open' should be `file does not exist'.
The word `refinements' at the end of the first paragraph should be `refinement'. A minor improvement to the first paragraph might be:
In the previous chapter we presented a theory of data refinement for partial and total relations. In this chapter we see how this theory may be extended to cover specifications written in the schema notation. Each operation schema corresponds to a relation on states, and an operation is correctly refined exactly when that relation is correctly refined. In this way, our existing refinement rules can be restated in terms of schemas.
There are two primed occurrences of ListRetrieveSet that should be unprimed - in the 2nd and 4th refinement conditions - they are easily spotted, as there are no primed variables in scope at that point.
Exactly the same error as on Page 263, except that now we are talking about the schema SumSizeRetrieve.
The first simulation rule in the table has lost its primes: it is properly primed where it appears in the text, further down the same page.
There is a diagram with a number of dotted lines. One of the lines, the hoop between 0 and 5 in the middle, is solid when it should be dotted in the same way as the line from the Blocked box (it is a continuation of this line).
There are four instances of report that should be suffixed with an exclamation mark: report!.
We state that the save area will behave as a first-in first-out buffer. We then go on, correctly, to implement it as a stack. Last-in first-out is what we meant.
The phrase `that, when will behave accordingly' should read `that will behave accordingly'.
There is an empty label [] to the right of the page.
What is more, the top of the page includes the phrase `sing the
guards'. Although this is quite evocative, it should read `using the
guards'. (In the second printing, it reads `with the guards'.)
The names of Mark Adams, Satoru Asakawa, and Alice King-Farlow should be added to the list of thanks.
| text | slides | exercises | solutions | cards | contents |