magistraleinformatica:mod:errata-2016:start

Lecture notes: a monograph is under preparation, earlier drafts of the chapters are made available here (with errata).

See main page for updated versions of the teaching material.

- Chapter 1: Introduction (draft)
- P17, page top: paramters should be parameters
- P17, line above Exercise 1.2: e
_{0}should be e_{1} - P19, functional code: fibiter should be fibaux

- Chapter 2: Preliminaries (draft)
- P34, page bottom: chek should be check
- P36, Example 2.4: x in E is repeated twice in the premises, the premise y in E is missing

- Chapter 3: Operational semantics of IMP (draft)
- P60, mid page, rightmost part of the conclusion: y:=(y+1) should be y:=(y-1)
- P64, page bottom: while x >= 0 do x := x-1 should be while x != 0 do x := x-1
- P66, first case: (iftt) should be (whtt)
- P66, second case: (ifff) should be (whff)
- P66, second case, line 1: \sigma(x)\neq 0 should be \sigma(x)=0
- P70, end of derivation: <[] should be []

- Chapter 4: Induction and recursion (draft)
- P78, proof of Lemma 4.1, first implication: ⇐ should be ⇒
- P86, line -12: m
_{1}should be m'_{1} - P87, line -7: tha should be that
- P88, rule 4.10: there is a misplaced dot in the premise
- P91, line 13: 1≤i≤n should be 1≤i≤k
- P93, mid page: the symbol c in the pair (b,c) should be existentially quantified

- Chapter 5: Partial orders and fixed points (draft)
- P101, towards page bottom: inerently should be inherently
- P107, Def. 5.7, line 3: of P should be of Q
- P110, Example 5.12, line 3: n should be x
- P112, line -3: missing closed parenthesis after “Figure 5.4”

- Chapter 6: Denotational semantics of IMP (draft)
- P129, two lines above Def. 6.2: function. should be function,
- P136, line -1: C[c
_{0}] should be C[c_{0}]\sigma - P135, line -3: b should be b
_{0} - P137, mid page: “of type is” should be “of type”
- P139, Example 6.8, definition of Gamma: B[x\neq 0] should be B[x\neq 0]\sigma

- Chapter 7: Operational semantics of HOFL (draft)
- Chapter 8: Domain theory (draft)
- P179, line 2: (d
_{i},e_{i}) should be {(d_{i},e_{i})}

- Chapter 9: Denotational semantics of HOFL (draft)
- P202, line 1: induction should be inductive

- Chapter 10: Equivalence between the operational and denotational semantics of HOFL (draft)
- Chapter 11: CCS, the calculus of communicating systems (draft)
- P226, definition of ENDCELL: input on gamma should be output on gamma
- P234, mid page: is x does should be if x does
- P246, line 3: fro should be for
- P247, statement of Theorem 11.4: if should be is
- P249, line -10: (p,q
_{m}) should be (p',q_{m}) - P256, explanation of diamond op: satisfies and the should be satisfies the
- P264, item 1: string should be strong

- Chapter 12: Temporal logics and the mu-calculus (draft)
- P281, end of line 3: \nu x.\mu\phi should be \nu x.\phi
- P281, mid page: a dot is missing before This
- P286, Problem 12.2, item 1: in should be is

- Chapter 13: Pi-calculus (draft)
- P289, abstract: ingenuous should be ingenious

- Chapter 14: Measure Theory and Markov Chains (draft)
- P320, line-9: X
_{1}should be X_{t} - P322, end of last line: a
_{i,i+1}should be a_{si,si+1} - P326, line -12: \mu should be l (twice)
- P328, mid page: \gamma_M should be \gamma_D

- Chapter 15: Discrete Time Markov Chains with Actions and Non-determinism (draft)
- Chapter 16: PEPA (draft, optional reading)

magistraleinformatica/mod/errata-2016/start.txt · Ultima modifica: 26/05/2016 alle 21:20 (6 anni fa) da Roberto Bruni