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

抽象によるソフトウェア設計−Alloyではじめる形式手法−

今日から第6章 「事例」に入ります。具体的な例を挙げている章です。実は本編は第6章で終わりなのですが、ページ数的にはまだ半分少し過ぎただけで、たくさんの付録があります。第6章を読み終えたら付録も内容に応じて読んでいこうと思います。

• 1つめの事例 - リーダー選出アルゴリズム
  • リング構造で接続されているプロセスがリーダーを決めるアルゴリズム(分散プロトコルの話題)
  • 固有の識別子(たとえばMACアドレス)が割り当てられているとする
  • 並列性と順序の保証がされないことを盛り込んだモデルにしてアルゴリズムを検証する
  • 時系列のイベントを表現するために Time シグネチャを導入して「あるイベントが起きた時刻」を関係として表現する
    • 時刻(Time)を多項関係の最後のタプルの最後のアトムにする。これは宣言をみると奇妙だけど使うところで自然な表現ができる
  • 述語(pred)で初期状態(init)、各時刻ステップの処理(step or skip)を記述して使う
  • プロセスの構造(リング状)、リーダー選出(DefineElected)、アルゴリズムのステップ全体(Traces)を fact として宣言する
  • skip があるために、すべての時刻でなにも起きないというのを避けるため、プールにトークンがあったら必ず何かアクションが起きること(skip の否定)を述語(pred)として宣言して使う