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

今日は 6.2 ホテルの客室施錠 からです。

• 「再コード可能錠」を使った使い捨て客室鍵の運用管理のシステムのモデル化
  • 錠前が疑似乱数列を用いて「現在の鍵の組み合わせ」と「次の鍵の組み合わせ」を持っており、「次の鍵」で開かれると状態が更新される
  • やはり Time シグネチャを導入
  • Key も ordering で順序つきに
  • Room, Guest をシグネチャ、FrontDesk を一元シグネチャとして宣言
  • Room <: keys in Room lone -> Key => Room と Key を関連付ける keys フィールドが単射であることを表現
  • 客が部屋を空ける時の述語は、錠前(つまりRoom)の状態変化と、他の状態が変化しないことを制約として記述する
  • チェックアウトは単に FrontDesk の客室の状態を変更するだけ(この状態ではまだ錠前の状態は変化してない)
  • チェックインは FrontDesk の客室と鍵番号の状態を変更し、客に鍵を渡す(Guest.keys に追加される)。この時もまだ錠前の状態は変化していない
  • Traces で時系列でチェックイン、入室、チェックアウトが連なることを宣言
    • first は初期化の述語(init)で初期化、最後の時刻を除く(Time - last)を忘れない
  • モデルの中で、不正な入室ができないことは明示的には宣言されていない(入室の述語 entry の前提条件で暗に導かれる)

今日はホテルの例のモデリングまで。続きの解析は次にします。