# DidaWiki

### Strumenti Sito

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: e0 should be e1
• 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: m1 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[c0] should be C[c0]\sigma
• P135, line -3: b should be b0
• 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: (di,ei) should be {(di,ei)}
• 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,qm) should be (p',qm)
• 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: X1 should be Xt
• P322, end of last line: ai,i+1 should be asi,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 (7 anni fa) da Roberto Bruni

### Strumenti Pagina 