Software AbstractionのVDM-SL例に間違い？



p.323のEnter関数の事後条件で、
c.fst = locks(r) and locks = locks~ ++ {r |-> c.snd}
という部分は、
c.fst = locks~(r) and locks = locks~ ++ {r |-> c.snd}
ではないか？

Posted: 月 - 10月 2, 2006 at 03:05 午後          

©