An introduction to Alloy

_main.md

Alloy 事始め

Software Abstractions の邦訳、抽象によるソフトウェア設計を読み始めた。 Part 2

形式手法と Alloy

適切な抽象は要だ。良い抽象は、柔軟さと理解しやすさを保つ。

抽象化のあとに具体化を行うことが理想に思える。しかし、設計時の環境が自然言語であると厳密さがない。具体化するとき抽象は崩れることがある。 そこで導入された手法がエクストリームプログラミングXPだ。これは設計と同時に開発することで抽象を保証する。 ところが、多くのプログラミング言語は冗長なため、少しの設計変更でも多くの編集を生む。

そのような問題を解決するため、思索向きで厳密な記法を採用した形式仕様記述が考え出され功績を挙げた。 だが普及に障壁があった。デバッグ機能の少なく、型検査とフォーマット印字が提供される程度だったため、使うには労力を要した。 Alloyは有限の空間を探索することを引き換えに、自動的にフィードバックを得られるようにできている。 有限と言っても、テストで達成できない大きさの空間を探索できる。さらに、テストケースを必要とせず満たすべき性質を記述すればよい。 XPに由来する即時性と形式仕様に由来する明瞭さが組み合わさっている。

住所録の例

まずはメールアドレスに別名をつけたデータベースを考える。fst_alloy.als に最小のコードがある。

シグネチャsignatureとはオブジェクトの集合で、addrのようなフィールドを持てる。あるBook bでNameからAddress への対応をb.addrと表す。述語predicateは取りうる状態を制限する。コマンド、例えばrunによって具体例を見つける。

２つめのコードは操作 operationと検査 check そして操作を組み合わせたときの アサーション を記述する。アサーションとはどんなときも真を満たす制約だ。反例があるかどうかを検査し、意に反し見つかる。 このSVGファイルは、File > Export To > Dotで書き出し dot -Tsvg counter-example.dot -o counter-example.svg で生成した。

反例はモデル（記述）の欠陥を示すこともあるが、これはアサーションのほうが間違えていそうだ。

実行方法

1. VSCode で構文ハイライト
2. Terminal > Run Build Task (事前に後述するTaskを定義しておく)
3. Alloy IDEでリロードし実行する。

Run Build Task

1. Ctrl+P >tasks: configure default build task
2. tasks.jsonを貼り付ける

Execute したら自動的に可視化する

Edit > Preference > Miscellaneous > Visualize automatically

トレースを使って好ましくない状況が発生する過程を調べる

アドレスに順序付けを導入し、状態遷移系列を可視化する。これには util/ordering を用いる。

counter-example.svg

fst_alloy.als

module tour/addressBook1

sig Name, Addr {}
sig Book {
    addr: Name -> lone Addr // 高々1つのAddrに対応する
    }

pred show (b: Book) {}

run add for 3 but 1 Book

tasks.json5

{
  // See https://go.microsoft.com/fwlink/?LinkId=733558
  // for the documentation about the tasks.json format
  "version": "2.0.0",
  "tasks": [
    {
      "label": "open",
      "type": "shell",
      "command": "java -jar /opt/alloy/Alloy.jar ${file}",
      "group": {
        "kind": "build",
        "isDefault": true
      }
    }
  ]
}

wrong_assertion.als

module tour/addressBook1

sig Name, Addr {}
sig Book {
  addr: Name -> lone Addr
  }

pred show (b: Book) {
  #b.addr > 1
  #Name.(b.addr) > 1
  }

run add for 3 but 1 Book

pred add (b, b': Book, n: Name, a: Addr) {
  b'.addr = b.addr + n -> a
}

pred del (b, b': Book, n: Name) {
  b'.addr = b.addr - n -> Addr
}

// 間違えた assertion
assert delUndoesAdd {
  all b, b', b": Book, n: Name, a: Addr |
    add [b, b', n, a] and del [b', b", n] implies b.addr = b".addr
}

// 正しそうな assertion
// assert delUndoesAdd {
//   all b, b', b": Book, n: Name, a: Addr |
//     no n.(b.addr) and add [b, b', n, a] and del [b', b", n] implies b.addr = b".addr
// }
check delUndoesAdd for 10 but 3 Book