Alloyで書こう：ドアロック仕様検証

今回は少し仕事っぽく。
IPAスライド [中小企業の形式手法への取り組み](https://www.ipa.go.jp/files/000005327.pdf) 内で紹介されている「試用例:ドアロック仕様検証」を書いてみる。

# 仕様

1. 車速、ドライバ席のオールロックボタン、チャイルドロック設定(リア席左右)で  
  ドライバ席、コドライバ席、リア左席、リア右席の4つのドアが開錠が可能かチェックする
2. ドライバ席は車速が15km/hを超えている場合のみアンロック不可
3. コドライバ席はドライバ席の条件に加えてドライバ席のオールロックボタンがONの場合アンロック不可
4. リア席は2、3の条件に加え、左右それぞれのチャイルドロックがONならばアンロック不可

# まずはそのまま書く

まず、上の仕様をそのまま書くとこうなった。
とは言っても 15km/h という具体値は書かず、抽象化する。

```alloy:あえてそのまま版
enum Speed {High, Low}
one sig Car {speed: Speed}

enum YesNo {Yes, No}
enum LockState {On, Off}
abstract sig Door {unlockable: YesNo}
one sig Driver extends Door {allLock, childL, childR: LockState}
one sig CoDriver, RearL, RearR extends Door {}

fact {
    Car.speed=High <=> Driver.unlockable=No     // 2.
    (Driver.unlockable=No || Driver.allLock=On) => CoDriver.unlockable=No   // 3.
    (CoDriver.unlockable=No || Driver.childL=On) => RearL.unlockable=No     // 4.
    (CoDriver.unlockable=No || Driver.childR=On) => RearR.unlockable=No     // 4.
}

run {}
```
書いている時点で結果例に見る問題点には気づいている。
それが形式仕様記述をすることで最初に得られる効果だ。

＃つまり「それって、プログラム書く立場になればすぐ気づくよね？」ということだ。
　しかし実際プログラムを書く側からすると、細かい点まで全部指摘することはできないし、
　別の場所で規定されたり隠れた意図があるかもしれず、仕様にない部分を勝手に解釈するのもリスクだ。
　プログラムを書く立場になって気づくべきなのは、やはり仕様を書く人なのだ。

# 結果例

車速15km未満、運転席の各ロックボタンは全てOFFという状態の例

![door1.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/20005/c3f92370-a9ef-e213-f033-37c87b747da5.png)

リア右席がアンロック不可になっているのは意図とは異なるだろうが、これでも「仕様通り」である。
なぜこうなるかと言うと、仕様 3, 4 に「さもなければアンロック可能」と書かれていないから。
少々厳しいようだが仕様不明確による問題で、仕様バグと言える。
こういった「常識だろう」という思いによる不明確さが後にバグとしてあらわれ、仕様ミスかコーディングミスかと揉める原因となる。
どちらに落ち着いたとしても余計な工数がかかってお互いに不幸だ。
　
日本語による論理記述が「明確に」両含意になっていないためだが、そこを含めて明確に記述すべきというのが形式仕様記述の立場。
というか、仕様の言い回しが 2「場合のみ」 3「場合」 4「ならば」と少しずつ変わっているのは、形式仕様記述を行うことでこの問題に気づいたという事例にするためではないだろうか。
VDM-SLで試したという記述がどうだったのか確認できないのが少し残念。

# 修正版

3, 4 も両含意に変えて、意図通りになっているか確認しよう。

```alloy:仕様明確化版
enum Speed {High, Low}
one sig Car {speed: Speed}

enum YesNo {Yes, No}
enum LockState {On, Off}
abstract sig Door {unlockable: YesNo}
one sig Driver extends Door {allLock, childL, childR: LockState}
one sig CoDriver, RearL, RearR extends Door {}

fact {
    Car.speed=High <=> Driver.unlockable=No
    (Driver.unlockable=No || Driver.allLock=On) <=> CoDriver.unlockable=No
    (CoDriver.unlockable=No || Driver.childL=On) <=> RearL.unlockable=No
    (CoDriver.unlockable=No || Driver.childR=On) <=> RearR.unlockable=No
}


check speed {
    Car.speed=High => Door.unlockable = No      // all door safelocked
    else Driver.unlockable = Yes
}
check allLock {
    Car.speed=Low => {
        Driver.allLock=On => {
            CoDriver.unlockable = No
            RearL.unlockable = No
            RearR.unlockable = No
        } else {
            CoDriver.unlockable = Yes
        }
    }
}
check childLock {
    CoDriver.unlockable=Yes => {
        RearL.unlockable = (Driver.childL=On => No else Yes)
        RearR.unlockable = (Driver.childR=On => No else Yes)
    }
}
```
`check`は`fact`と違う形で、なるべく別の視点で確認するよう書いた。
今度は問題ない。

# 書き直そう

今回の仕様でドア自体は特に意味を持たないので、車に直接結びつけてもよいだろう。

```alloy:リファクタ版
enum Speed {High, Low}
enum Switch {On, Off}
enum LockState {Unlockable, SafeLocked}
one sig Car {
    speed: Speed,
    allLock, childL, childR: Switch,
    driver, coDriver, rearL, rearR : LockState
} {
    speed=High <=> driver=SafeLocked
    (driver=SafeLocked || allLock=On) <=> coDriver=SafeLocked
    (coDriver=SafeLocked || childL=On) <=> rearL=SafeLocked
    (coDriver=SafeLocked || childR=On) <=> rearR=SafeLocked
}

run {}
```

```txt:結果例：CarにまとめたのでTableViewの方が見やすい
┌────────┬─────┬───────┬──────┬──────┬───────────┬───────────┬───────────┬───────────┐
│this/Car│speed│allLock│childL│childR│driver     │coDriver   │rearL      │rearR      │
├────────┼─────┼───────┼──────┼──────┼───────────┼───────────┼───────────┼───────────┤
│Car⁰    │Low⁰ │Off⁰   │On⁰   │Off⁰  │Unlockable⁰│Unlockable⁰│SafeLocked⁰│Unlockable⁰│
└────────┴─────┴───────┴──────┴──────┴───────────┴───────────┴───────────┴───────────┘
（enum Speed, Switch, LockState の表示は省略した）
```

# 参考

- IPAスライド [中小企業の形式手法への取り組み](https://www.ipa.go.jp/files/000005327.pdf)