抽象によるソフトウェア設計 付録A 練習問題 その22

付録A.5 の小さなケーススタディの鉄道のスイッチングです。
かなり久しぶりになってしまいました。スイッチングポリシーのチェックをやってみました。

• 現在 Train が占有している Segment へ入る信号を全て侵入禁止にするという厳しい条件でやってみました。また trainsit で

pred NoConflict (ts: TrainState) {
  all disj t1, t2: Train {
    no ts.occupied[t1] & ts.occupied[t2]
  }
}

pred gatePolicy (ts: TrainState, gs: GateState) {
  all t: Train {
    ts.occupied[t] in gs.closed
  }
}

assert GatePolicyIsSafe {
  all ts: TrainState - last {
    let ts' = ts.next {
      all gs: GateState | all t: Train {
        (NoConflict [ts] and gatePolicy [ts, gs] and transit [ts, ts', gs, t])
          => NoConflict [ts']
      }
    }
  }
}
check GatePolicyIsSafe for 6

• • assert の時に多重度をつい one や some にしてしまうのですが、「A ならば B」という述語で前提条件(A)を加えているので all でいいんでした。慣れないとすぐ忘れてしまいます

さて、ずいぶん長いあいだ読んできた「抽象によるソフトウェア設計」ですが、残りの付録A はかなり難しい問題で、その先はリファレンスと他の処理系の話なので、ここで一旦終了としようと思います。
Alloy はプログラミング言語とはちょっと違う世界をみせてくれました。しかし当初考えていた証明システムというよくわからないなにかというイメージとは少し違っていて、述語を正しく記述するのは難しいことは難しいですがルールに違反する組み合わせを指定された範囲内で網羅検査するとういう動作原理はシンプルで納得しやすいものでした。これですぐ実務のシステムの検証にAlloyが使える! とまでは思えませんがこれからソフトウェアの設計をする上で反例を探して欠陥を直すというプロセスは意識したいです。

次は「Webを支える技術」にしようと思います。しかししばらく時間に余裕がない日が続きそうなので、更新は不定期になります。