抽象によるソフトウェア設計 第6章 事例 その3

今日は 6.2.3 ホテルの客室施錠の解析のところからです。

• 不正な入室がないことの assert
  • 「客がある時刻に入室する(錠前を開ける)時、フロントでその部屋に*宿泊客が登録済みなら*その客が登録されている」
    • ちょっとまわりくどくなっているのは客室錠前のシステムの性質による。客がチェックアウトしても次の客が次の鍵で錠前を開錠するまでは古い鍵で入室できる
    • そして反例がみつかる。たとえ新しい客がチェックインした後ですら、次の鍵で開錠する前なら古い鍵で入室できてしまう
      • ちなみに実際に Alloy がみつけた反例は最初の客は入室すらする前にチェックアウトして、次の客のチェックイン後に入室してる。この反例から客がチェックインしたのに入室せずにチェックアウトすると次の客が入室できないという問題にも気づかされますね
  • チェックインしたらすぐにその客の入室が起きる、ということを制約(fact)として導入する
    • しかしこの制約には無理があるような気もする。この施錠システムに問題があると考えるべきなような

この例はソフトウェアシステムに限らず、「手順」の不備を探すことができるということを示しているようですね。Alloy での解析するモデルは必ずしもソフトウェアとして実現されるものに限らないようです。
次はまだこのホテルの客室施錠の事例で、イベントをシグネチャとする記述方法を例示するようです。