Strumenti Utente

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 (4 anni fa) da Roberto Bruni