正誤表

2011/11/10： 7章例題の不変条件（図7.17）

誤： 図7.17の不変条件に含まれるandで結ばれた4つのforall式のうち3つ目

(forall uid in set getAllUserIDs() &
      forall eid in set dom events &
          card getReservations(uid, eid) <= getEventMaxSeats(eid))

正

(forall uid in set getAllUserIDs() &
      forall eid in set dom events &
          card { res.getSeats() | res in set getReservations(uid, eid) }
            <= getEventMaxSeats(eid))

2011/11/10： 7章例題のreserve操作事前条件（図7.18）

誤： 図7.17の不変条件に含まれるandで結ばれた3つの式のうち2つ目

card getReservations(resinfo.getUserID(), resinfo.getEventID())
     + card resinfo.getSeats()
      <= events(resinfo.getEventID()).getMaxSeats()

正

card { res.getSeats() | 
       res in set getReservations(resinfo.getUserID(), resinfo.getEventID()) }
      + card resinfo.getSeats() 
    <= events(resinfo.getEventID()).getMaxSeats()