形式手法とアジャイル

　私は形式手法にはソフトウェアの品質を高める力があると信じている。一方、プロジェクトの進め方に関して言えばアジャイルのようなやり方が有効だと思っている。しかし、私が形式手法とアジャイルの両方に興味を持つ事に関して、そういう人は珍しいと言う意見を何度か耳にした。どうもアジャイルと形式手法が相容れないと考える人が多いようである。その気持ちは何となく分かるが、私としては両立すると思っているので、今日はその事を書きたい。

私の主張は以下の通りである。

アジャイルなプロジェクトで形式手法を活用する事ができる。

それに対して、よく（？）聞かれる反対意見は以下のようなものである。

1. アジャイルなプロジェクトでは、前払いの設計を行わない。形式手法を適応する場はないのではないか？
2. 設計で形式手法を使った場合通常より時間がかかるのではないか？その結果、開発の速度を落とすのでは？
3. テスト駆動開発で開発しているから検証は十分ではないか？
4. 形式手法のツールを使いこなすのが難しい。学習に時間がかかる。
5. 証明までしなくても良いのでは？過剰品質では？

以下、それぞれの反対意見に反論してみよう。

1. アジャイルなプロジェクトでは、前払いの設計を行わない。形式手法を適応する場はないのではないか？
　「アジャイルなプロジェクトでは、前払いの設計を行わない」と言われているが、まったく設計を行わないわけではない。確かに設計書とかアーキテクチャ説明書のような文書は作らないかもしれないが、プログラマが実装する（まさにソースコードを編集する）前には頭の中で設計という行為が行われている。そこでは、メソッドや変数の名前を決めたり、クラス間の関係を考えたり、クラスの状態遷移を思い浮かべシミュレーションしたりする。これらはその結果を文書の形で残さなくても立派な設計行為である。そして、この設計した結果を検証するのに形式手法を用いる事ができる。特に振る舞いを検証するときには形式手法のツールが役に立つだろう。

2. 設計で形式手法を使った場合通常より時間がかかるのではないか？その結果、開発の速度を落とすのでは？
　確かに設計に費やす時間が増える可能性はある。しかし、仮に設計に多くの時間がかかったとしても従来のやり方では設計段階で見つけられなかった不具合を見つける事ができれば、デバッグと修正にかかる時間が削減できるためトータルでは時間を短くすることができる。形式手法やツールについて不慣れなうちは設計にかかる時間が従来に比べてかなり多くなるだろうが、それは経験を重ねることによって徐々に改善される。私は何度か実プロジェクトでモデル検査を使用した事があるが、以前マルチスレッドのライブラリにおける関数呼び出しとコールバックについてデッドロックが起きないかをSPINで検証したときは、スクラッチからモデルをつくって検証を終えるのに約1時間であった。同じことをテストでやったとしても同程度の時間がかかるのではないかと思う。しかもテストではなかなか網羅的にテストすることは難しいが、モデル検査ならば全ケースを網羅的に調べてくれる。

3. テスト駆動開発で開発しているから検証は十分ではないか？
　十分ではない（ことがある）。理由は、網羅的にテストをすることは（主に時間の都合で）難しく、その結果不具合を見逃す事があるからである。テスト駆動開発で書かれるテストは決して十分ではない。テスト駆動開発のテストは単体テストとは異なり、網羅して不具合を出し切ることが目的ではなく、実装にあたり大きな考え違いはないかを見つけたり、使用者にとって使いやすい仕様になっているか確認したり、そして実装者に少しだけの自信を与えるたりするものである。検証という点では十分とは言いがたい。

4. 形式手法のツールを使いこなすのが難しい。学習に時間がかかる。
　確かにそういう点はある。しかし、先日IPAで開催されたVDMのセミナーによると一週間の教育期間をもうければ、あとはエキスパートの助言を受けながら開発をすることはできるという。そのセミナーでも言われていたのだが、自分のものにするには教科書の問題である程度練習したら、実践することが一番である。実際のプロジェクトで頭をフル回転させながら挑めば、あっという間に上達するだろう。そして上達した暁には、以前より正確なプログラムを速く開発できるようになる。ということでこの意見に対しては、最初は時間はかかるだろうけど、そのうち学習時間を取り消すくらいの効果がある。というのが私の意見である。

5. 証明までしなくても良いのでは？過剰品質では？
　確かにプログラムの正当性を証明するとなるとツールのサポートがあったとしても時間がかかるだろう。そしてその時間と結果として担保される品質を天秤にかけたとき、過剰品質となる場合はある。しかし、形式手法だからといって必ずプログラムの正当性を証明しないといけない訳ではない。たとえば、モデル検査は有限の状態空間がある性質を保持するかを検査する方法で、証明よりもずっと手軽にできる。マルチスレッドやマルチプロセスのシステムでは、テストではタイミングに依存するため不具合を捕捉しきれないことがあるが、モデル検査を使えば網羅的に検査する事ができる。またAlloyというツールを使えば、仕様に暗黙の前提を置いていないかとか抜けや漏れがないかを確かめる事ができる。それぞれの手法（ツール）には得意とするところがあり、求める品質と対象のシステムの特徴をよく考えて、適した手法を用いれば過剰品質という状態は避けられるだろう。

以上の議論から私を主張をまとめると以下の通りである。

アジャイル開発においても形式手法を用いる場面はある。ただし、最初の学習段階ではエキスパートの助けがあった方がいいことと問題に適した手法を採用することが大事である。

2012年に形式手法を学び始めるならこの7冊

前エントリー「僕が形式手法を学び始めたときに読んだ10冊 - masaterukの日記」のラインナップはあまりに入手困難なものばかりだったので、2012年に始めるならということで改めて選んでみた。

１冊目。

VDM++によるオブジェクト指向システムの高品質設計と検証 (IT architects’ archive)

VDM++の本。形式手法を学び始めるならこの本から始めると取っ付きやすいのではないかと思う。高級言語をつかった陽関数定義（実行可能形式）でモデルをがんがん書いて、シミュレーションとテストでモデルを洗練していくやり方は実際の現場にあっているように思う。関数型プログラム言語をひとつやふたつやったことある人なら、すいすいモデルをかけるんじゃないだろうか。

2冊目。

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

Alloyの本。前回のエントリーで紹介した通りなんだけど、訳本は第2版をベースにしていて中身も充実。上記のVDM++の本では陽関数定義でがんがん書いていくけど、Alloyでは陰関数定義でモデルを記述する。陰関数定義は、陽関数定義とは違って単に関係を記述する。方程式で例えるとx = から始まるような解を書く必要はなく方程式のままにしておくような書き方（だから解の公式を知らなくてもモデルが書ける）。関係しか記述しないと実行可能ではないのでVMD++のようにシミュレーションできないように思えるが、Alloyはそのモデルを例を示す事でシュミレーションを可能にする。形式的仕様記述の腕を上げたいならAlloyがおすすめ。

3冊目。

SPINモデル検査入門

Spinの本。これも今では日本語で解説している本がたくさん出ている。残念ながら全部目を通していないので自分が読んだ物の中から一冊選んだ。この本は、Spinをつかってモデル検査ができるようになることを目的とした本。裏側にある理論や機構については最小限にとどめツールを利用する事に主眼を置いた本。最初に始めるにはホルツマンの本ではなくこの本で良いのかもしれない。モデル検査は学べばすぐにでも現場で使える技術。

4冊目。

オブジェクト指向入門 第2版 原則・コンセプト (IT Architect’Archive クラシックモダン・コンピューティング)

メイヤーさんのオブジェクト指向入門第2版。残念ながら第2版は未読。第一版の内容をさらに充実させているだろうから間違いないと思う。契約による設計（Design by Contract）を学ぶんだったらこの本以外はないと思うし、契約による設計がソフトウェアの品質をぐっとあげてくれるだろうと思うので、やっぱり避けられない一冊。

5冊目。

Bメソッドによる形式仕様記述―ソフトウェアシステムのモデル化とその検証 (トップエスイー実践講座)

Bメソッド。これも未読。今からやるならリファインメント（詳細化）はおさえておきたい。やるならBメソッドかEvent-Bになるだろう。ちゃんとやるならどっちもやることになるだろうけど、「最初は日本語の本で始めたい」というならこの一冊かな。

6冊目。

Concurrent and Real-time Systems: The CSP Approach (Worldwide Series in Computer Science)

CSP。実は前エントリーで紹介したホーアの本「ホーアCSPモデルの理論」より読みやすい。CSPをやるならこの本から初めて"The Theory and Practice of Concurrency"に進むのが良いのかな。もう一度言うと、マルチスレッドやマルチプロセス、またはネットワーク越しにメッセージをやりとりするシステムを作っているならCSPはやっておいた方がいい。

7冊目。

Logic in Computer Science: Modelling and Reasoning about Systems

ここまでホーア論理を解説している本がなかったので最後にこれを選んでみた。自分は未読なんだけど一時期自分のまわりですごく流行った本。これで基本的なところをおさえるのがいいと思う。英語が苦手ならば、Coqを触りながら「ソフトウェアの基礎」を読み進めるのもいいかもしれない。

ということで、今回は以上7冊。

僕が形式手法を学び始めたときに読んだ10冊

後輩に形式手法を学び始めたときに読んだ本を紹介すると約束したので、せっかくなのでブログに書くことにした。
形式手法を学び始めたのは2004年だから、今から始める場合はまた違ったラインナップになるだろうけど。
※「2012年に形式手法を学び始めるならこの7冊 - masaterukの日記」を書きました。

1冊目。

プログラミングの科学 (情報処理シリーズ)

出会いはこの本。僕の人生を変えてしまった本だ。この本に出会ったときの衝撃は今でも覚えている。命題と述語からはじまり、ホーア論理、そしてプログラムの作り方が解説してある。「プログラムの作り方」を解説している本は少ない。Twitterでもつぶやいたけど、assertの使い方を教えてくれたのもこの本だった。現在は入手困難だけど、何とか手に入れて読んでほしい。

2冊目。

ソフトウェア開発のモデル化技法

仕様記述言語VDM-SLの本。VDMはツールもあるので、モデルを書きながら読み進めるといいだろう。この本でよく覚えているのは「第1章　序章」。序章を読んで、何となく内容を理解したつもりになっていたけど、実は全然理解していなかったってことに後で気づいたのを覚えている。”仕様”や”設計”ってソフトウェア開発しているとなじみのある言葉だから軽く読み流してしまうんだけど、そうやって読んでいるといつまでも理解が深まらない。本は一言一句大切に読むべきということを学んだ本。なお、VDMのモデルをみて「これなら直接プログラム書くのと変わらない」と思ったらまだまだだと思った方が良い。

3冊目。

ソフトウェア仕様記述の先進技法 Z言語

こちらはZの本。上の2冊を読んでいれば割とすんなり読めるかな。この本には、仕様とプログラムが満たすべき関係と詳細化についての解説がある。今ならBメソッドをやった方がいいのだろうか。この本を読んでた頃、ZやVDMで自分たちが開発しているシステムのモデルを書いて、最弱事前条件を計算していたりしたっけ。

4冊目。

コンピュータサイエンス入門〈2〉論理とプログラム意味論

リアクティブシステムについて日本語で学べる貴重な本。これも絶版なのか…。リアクティブシステムとは、外部環境とやりとりしながら動き続けるシステムのこと。作られるソフトウェアの多くがリアクティブシステムと言えるだろう。リアクティブシステムのプログラム、意味論、時相論理による仕様記述と検証について学べる。薄いけど内容が濃く、何度も読み直した（読み直さないと理解できなかった）本。

当時は、上記4冊がいわゆる必須科目と言われていた。この4冊は何度も読み返した。

5冊目。

論理学をつくる

論理学の本。どの本もだいたい命題と論理から説明してあるんだけど、どうもそのあたりの理解が怪しいので買った本。戸田山先生の本はとても分かりやすて独学に向いている。これはまだ買える。良かった。

6冊目。

オブジェクト指向入門 (ASCII SOFTWARE SCIENCE Programming Paradigm)

オブジェクト指向の名著。ZやVDMで書くモデルと自分たちが開発しているオブジェクト指向ってどういう関係にあるか分からなくて、オブジェクト指向を特定のプログラム言語によらずに勉強したくて読んだ本。まぁ、Eiffelって言語なんだけどw 説明が明解でわかりやすい。形式仕様記述を学んだあとだと契約による設計は非常になじみやすい。形式手法に興味なくてもオブジェクト指向やるんだったらこれは読んでほしい。

7冊目。

ホーアCSPモデルの理論

ホーアのCSPの本。マルチスレッドやマルチプロセスといった並行システムのモデルの本。CSPを使えば、並行に動作するプロセスを組み合わせたときに全体としてどういう振る舞いになっているか？を計算でき、仕様を満足しているか検証できる。しかも、証明で。パフォーマンスが求められるシステムではマルチスレッド、マルチプロセスになることは避けられないだろうし、オブジェクト指向システムをオブジェクトが相互作用するシステムと捉えることもできるので、CSPの適用範囲は広いのではないかと見ている。逆に、こういったモデルなしに並行システムを検証する事は不可能だろう。

8冊目。

計算機プログラムの構造と解釈

SICP。今さら紹介するまでもないんだけど、自分の印象はプログラミングに関する概念を一通り学べる本といったところ。当時、CやC++などの手続き型言語しか知らなかったので、高階関数や遅延評価、継続といった概念には「へぇ」って思った。決して仕事で使わなくても、こういう概念を知っていると知らないとでは生み出すプログラムが違うんじゃないだろうか。

9冊目。

SPIN Model Checker, The: Primer and Reference Manual

モデル検査器SPINの本。これまた自分の人生を変えた本。はじめて現場で適用したのがSPINだった。マルチプロセスでやりとりするプロトコルの設計をまかされて、「こりゃ大変じゃ」と思って、まだデッドロック検出（SPINはデフォルトでデッドロック検出をしてくれる）とassertしか使えない状態でPromelaで書き始めた。書いて検査すると非常に優秀なレビューアといっしょにペアモデリングをやっているような感覚がある。モデル検査は実際の現場で適用しやすいと思う。SPINを徹底的に学びたいならこの一冊だろうな。

10冊目。

Software Abstractions: Logic, Language, and Analysis

Alloyの本。形式的に仕様を表現して、その仕様を満足するプログラムを作ったとしても、仕様が自分が欲しているものと異なっているとせっかくのプログラムも意味がない。だから書いた仕様が自分が欲しい物なのかを確認したい。Alloyはそれができるツール。自分が記述したモデルを満たす例を示してくれる。こういうツールは容赦がなくて、「そういうつもりじゃないんだよ」って言いたくなるような例をいっぱい示してくれる（そういうときは仕様の記述が足りないからバグとなりうる）。この本は、第２版の訳本『抽象によるソフトウェア設計−Alloyではじめる形式手法−』が出ているので、今やるなら訳本を読めば良い。

以上、10冊。

多相型をサポートしました ー OCamlをC言語に変換するプログラム ー

OCamlをC言語に変換するプログラム（今のところ、uCamlって名前にしてます）に機能追加しました。多相型のサポートです。

https://github.com/masateruk/micro-caml

これにより、以下のようなOCamlのプログラムをCのプログラムに変換できます。

let rec id x = x in
let n = if (id true) then (id 1) else (id 0) in
  print_int n

多相型のサポートによる恩恵は、上記プログラムにある id という関数です。これは引数 x をそのまま返すなんてことない関数ですが、注目してほしいのはその型です。型を調べるためにOCamlのインタプリンタに入力してみましょう。

$ ocaml
        Objective Caml version 3.12.0

# let rec id x = x;;
val id : 'a -> 'a = <fun>

val id : 'a -> 'a = と出ました。これは、id はある a という型を引数にとり、その型 a を結果として返す関数型である、ということを示しています。ここで a は型変数と呼ばれるもので、どんな型もとることができます。たとえば、int 型の引数を適応する場合は int -> int という型になり、bool型の引数を適応する場合は bool -> bool という型になります。インタプリンタで試してみましょう。

# id 0;;
- : int = 0
# id true;;
- : bool = true

こういった関数をC言語で実現するのは簡単ではありません。たいてい型の制約をさけるために void* を利用しますが、これだと引数を関数に適応する場合にキャストする必要があります。キャストした場合はコンパイラの型検査の恩恵をあずかることができません。たとえば、int 型の引数を適応した結果をbool 型の変数に代入するようなコードがあってもキャストしている場合はコンパイラはエラーを報告してくれません。しかし、OCaml（だけでなく一般的な関数型言語）ならば、こういった型エラーをコンパイル時に報告してくれます。uCamlでもOCamlと同様の型検査を行います。型検査を通ったものがC言語に変換されるため、生成されたC言語のプログラムには型エラーはありません。

一番上にあげたプログラムは以下の手順で C へ変換、コンパイル、実行できます。

$ ./ucaml id.ml -o id.c
$ gcc -Wall id.c -o id -I/usr/local/include -I. -lgc -L/usr/local/lib
$ ./id
1

ひとつだけ注意点があります。今回は、メモリ管理の部分をさぼって Boehm GC (http://www.hpl.hp.com/personal/Hans_Boehm/gc/) を使うようにしました。よって、生成した C のプログラムをビルドおよび実行するときには Boehm GC が必要になります。個人的には自分でメモリ管理するよりもこういった GC を利用した方がいいと思っているのですが、一応 Boehm GC に依存しないものも出力できるようにするつもりです。

OCamlをC言語に変換するプログラムをつくりました

MinCamlをベースにしてOCamlをC言語に変換するプログラムをつくりました。

https://github.com/masateruk/micro-caml

何でそんなものをつくったかと言うと、わたしは組み込みプログラムの開発を仕事にしているのですが、

• 自分はOCamlで開発したい（C言語の型検査は心もとない。OCamlの強力な型検査に守られてコードを書きたい）
• しかし、OCamlで書くと誰も引き継げないため、使わせてもらえない。

ということで、自分が書くときはOCamlで書いて、納品するときにCに変換すればいいんじゃないかと思った次第です。OCamlを書ける人がいるんだったらOCamlのコードを引き継いでもらえばいいけど、Cしかわかりませんな人には変換後のCのコードを渡すという作戦です。もちろん、変換後のCのコードを直接変更しちゃうとOCamlのコードは役に立たなくなるんですけど、それはしょうがないとします。

サポートしている構文要素はMinCamlよりもさらに少なく、基本型はInt型のみ。破壊的代入もありません。しかしクロージャはサポートしたので、以下のようなプログラム

let rec plus x =
  let rec add y = x + y in
    add in
  print_int ((plus 1) 2)

は次のようなCのプログラムに変換します。

#include <stdio.h>
#include <stdbool.h>

int _add_11_(int y_12_, int x_6_)
{
  return x_6_ + y_12_;
}

typedef struct {
  int (*f)(int, int);
  int fv1;
} c_13_t;

c_13_t make_c_13_t(int (*f)(int, int), int fv1)
{
  c_13_t tmp_r14;

  tmp_r14.f = f;
  tmp_r14.fv1 = fv1;
  return tmp_r14;
}

c_13_t plus_5_(int x_6_)
{
  c_13_t add_11_;

  add_11_ = make_c_13_t(_add_11_, x_6_);
  return add_11_;
}

int apply_c_13_t(c_13_t tmp_r15, int tmp_i16)
{
  return tmp_r15.f(tmp_i16, tmp_r15.fv1);
}

int main()
{
  int tmp_i1_10_;
  c_13_t tmp_f2_8_;
  int tmp_i3_9_;
  int tmp_i4_7_;

  tmp_i1_10_ = 1;
  tmp_f2_8_ = plus_5_(tmp_i1_10_);
  tmp_i3_9_ = 2;
  tmp_i4_7_ = apply_c_13_t(tmp_f2_8_, tmp_i3_9_);
  printf("%d", tmp_i4_7_);
  return 0;
}

テンポラリーな変数が多いのは、おそらくK正規化のためだと思います。変換先の言語がCなので、K正規化を適当にサボればもう少し読みやすいコードが出力できるようになるかと思います。

まだまだ機能が足りないのですぐに実用できるレベルではありませんが、入出力やリソース管理を除いたロジックを取り出して、その部分をささっとつくっちゃうようなことができないかと期待してます。

今後、他の言語要素もサポートしたいのですが、単純にOCamlの言語要素をサポートするのではなくモデリングやプロトタイプ時に役に立つような機能をたそうかなと考えているところです。
ねらいは、OCamlでモデリング（プロトタイプや検証など）してからC言語を生成です。

コマンドキューをもつシステムのAlloyモデル

とあることがきっかけで、コマンドキューをもつシステムをAlloyでモデル化し検証したので、ここで紹介します。

問題

あるシステムのミドルウェアを修正することになりました。このミドルウェアは整数値をやり取りするオブジェクトを複数所有します。インタフェースは以下の通りです。

• assign(v) 　　// オブジェクトの値をvに上書きします。
• copy(obj) 　　// オブジェクトobjの値をコピーします。
• getValue()　　// オブジェクトの値を取得します。

このミドルウェアを実装するためにライブラリを使用しています。このライブラリはオブジェクトを複数所有しています。各オブジェクトはキューを持ち、コマンドをキューに積んでから実行する必要があります。コマンドは2種類あります。

• assign(v)コマンドは、値の上書きする。
• copy(obj)コマンドは、オブジェクトobjの値をコピーする。

キューに積んだコマンドを実行するときはライブラリの関数

• execute()

を呼びます。executeを呼ぶとキューに積まれた順番にコマンドを実行します。オブジェクトの値は、これまたライブラリの関数

• get()

でいつでも（同期で）読みだせます。

当初の実装は以下のように、コマンドをひとつ積むたびにexecute()を呼びだすようになっていました。

void assign(int v)
{
    add_command(make_command(assign, v));
    execute();
}

しかしexecuteに時間がかかっていたので、なるべくコマンドをためてからexecuteをするように改良しようとなりました。

はじめは思いついたままに実装してテストをしていたのですが、テストの種類を増やすとうまくいかないものがぽつぽつ見つかるという状態が続いたので、Alloyで検証することにしました。以下では、モデルを検証しながらインクリメンタルに作った過程を再現します。

状態モデル

まずは、値、コマンド、オブジェクトをモデル化します。コマンドキューを表すのには seq を使いました。後々検査で使うために、オブジェクトが保持する値は、実際の値（real）と期待値（expexted）のふたつにします。

module CommandQueue

abstract sig Value {}
one sig Zero, One, Two extends Value {} 

abstract sig Command {}

sig Copy extends Command {
    src : one Object
}

sig Assign extends Command {
    v : one Value    
}

sig Object {
    expected : one Value,
    real : one Value,
    q : seq Command
}

pred show() {}
run show for 3 but exactly 1 Object

オブジェクトの数をひとつに制限して、[Execute]、[Show] の順番に実行します。以下のようなインスタンスが見つかりました。

[Next]を押して次々に出てくるインスタンスを確認します。想定外のインスタンスが見つからないので、ここまでは正しそうです。

assignとcopyを追加する

次に、assignコマンドとcopyコマンドをキューに積む操作を追加します。まずは、状態の変化を表すためにTimeシグネチャのorderingを導入します。

open util/ordering[Time] as to
sig Time {}

時間で変化する属性をTimeとの関係にします。

sig Object {
	expected : Value one -> Time,
	real : Value one -> Time,
	q : (seq Command)-> Time
}

時間変化をTimeを右側に持ってきた関係で表すので、多重度をシグネチャの右側に移動させます。コマンドキューが時間によって変化するので、seq Command 全体を括弧で囲みます。
assignコマンドは述語で表します。t が事前、t' が事後の時点を表します。この時点では期待値（expected）だけ変更し、実際の値は変更しません。

pred assign [t, t' : Time, obj : Object] {
     some assign : Assign | obj.q.t' = (obj.q.t).add[assign] and obj.expected.t' = assign.v and noChangeRealValue[t, t', obj]
}

述語 noChangeRealValue は以下の通り。いろんなところで使いまわしそうなのでひとつの pred として切りだしました。

pred noChangeRealValue [t, t' : Time, obj : Object] {
	obj.real.t' = obj.real.t
}

copyコマンドもほぼ同様です。

pred copy [t, t' : Time, obj : Object] {
     some cp : Copy | obj.q.t' = (obj.q.t).add[cp] and obj.expected.t' = cp.src.expected.t and noChangeRealValue[t, t', obj]
}

最後にこのシステムがとり得る状態遷移空間をfactで指定します。状態遷移空間は、初期状態から assign または copy コマンドによって遷移できる空間です。

pred init [t : Time] {
	all obj : Object | (no obj.q.t and obj.real.t = obj.expected.t)
}

pred noChangeAll [t, t' : Time, obj : Object] {
	obj.expected.t' = obj.expected.t
	obj.real.t' = obj.real.t
	obj.q.t' = obj.q.t
}

fact step {
	init[to/first[]]
	all t : Time - to/last[] | let t' = to/next[t] |
		one obj : Object |     // (a)
			(assign[t, t', obj]
			or copy[t, t', obj])
			and (all obj' : Object | obj' != obj => noChangeAll[t, t', obj'])  // (b)
}

fact step の (a) で one obj : Object、および (b) で (all obj' : Object | ...) としているのは、1ステップで状態遷移するオブジェクトをひとつに限定するためです。そうしておくとVisializeしたときに何が起きたか分かりやすくなります。ただし、同じTimeインスタンス数では、同時に複数遷移するモデルに比べて探索できる空間が狭くなるので、見つかってほしい反例が見つかりにくくなります。
今度はObjectのインスタンス数を 2 にして[Show]してみます。

pred show() {}
run show for 3 but exactly 2 Object

妙なインスタンスが見つからないので、ここまでは正しそうです。

executeを追加する

execute も述語で表します。

pred execute [t, t' : Time, obj : Object] {
     isEmpty[obj.q.t']
     let command = last[obj.q.t] {
		(command in Assign) => (obj.real.t' = command.v and obj.expected.t' = obj.expected.t)
		(command in Copy) => (obj.real.t' = command.src.real.t and  obj.expected.t' = obj.expected.t)
	}
}

これは、「キューは空で、キューの最後に積まれているのが assign だったら execute 後の real は expexted と同じ。copy だったら src の real と同じ。かつ、expected は変化しない。」です（察しのいい人は気付くと思いますが、これは間違っています）。
次に、fact step に execute を追加します。

fact step {
	init[to/first[]]
	all t : Time - to/last[] | let t' = to/next[t] |
		one obj : Object | 
			(assign[t, t', obj]
			or copy[t, t', obj]
			or execute[t, t', obj])
			and (all obj' : Object | obj' != obj => noChangeAll[t, t', obj'])
}

最初のモデル ー get前にexecuteする ー

一応、これで準備は整いました。では、executeの回数を減らした新しいミドルウェアの振る舞いを考えて、それを検証したいと思います。最初に考えたのは、以下のようにassignやcopyのメソッド内でexecuteを一切呼ばないことにして、getValueが呼ばれたときにgetする前にexecuteするようにしたらどうかと考えました。

void assign(int v)
{
    add_command(make_command(assign, v));
//    execute(); // <- 毎回呼ぶのを止める
}

int getValue()
{
    execute(); // <- get前に一度だけ呼ぶように。
    return get();
}

これはいつでもexecuteを呼べば、そのあとは正しい値を取得できるということを根拠にしています。よって、このことをアサートで検査してみます。execute 後は期待値と実際の値が一致するというアサートは以下のように書けます。

assert RealValueEqualsExpectedAfterExecute {
	all t : Time - to/last[] | let t' = to/next[t] |
		all obj : Object | 
			execute[t, t', obj] => obj.real.t' = obj.expected.t'
}
check RealValueEqualsExpectedAfterExecute for 3 but exactly 1 Object, 4 Time, 4 seq

まずはオブジェクト1個に限定して、[Execute]メニューからアサートを選んで実行します。そうすると以下のような反例が見つかります。

1. 初期状態は、Object.real = Object.expected = Two
2. Object.assgin(Zero). Object.real = Two, Object.expected = Zero
3. Object.copy(Object). Object.real = Two, Object.expected = Zero
4. Object.execute. Object.real = Two, Object.expected = Zero

これは、初期状態から、assign, copy(自分自身), execute と進んだ場合、assign で代入した値が無視されて期待値と実際の値が異なることを示しています。実際のシステムは execute した場合、キューのコマンドを順番に実行するわけですから、キューの先頭に入っている assign を実行した時点で期待値と実値が一致します。よって、そのあとに copy を実行すれば、copy 後も期待値と実値は一致します。ということは、execute のモデルが間違っていると言えます。

executeを修正する

では、executeを修正しましょう。今回は素朴にキューのすべてのコマンドをひとつずつ実行するように修正します。「ひとつずつ実行する」といっても、Alloyではループや再帰呼び出しを書けません。そこで、コマンドひとつを実行するたびにひとつ時点を進めるようにします。つまり、ある時点 t でコマンドキューに assign, copy と積まれていた状態で execute すると、t の次の時点(これを t' とします)ではassign実行後の状態、t' の次の時点ではcopy実行後の状態に遷移するとします。実際のシステムでは、execute はアトミックに実行されます。よって、モデル上でも execute しはじめたらキューが空になるまでの間はコマンドの追加できないようにします。これを実現するためにモデルに状態を表す変数を追加します。

sig State {}
one sig InitDone, AssignAdded, CopyAdded, Executing, ExecuteDone extends State {}

sig Object {
	expected : Value one -> Time,
	real : Value one -> Time,
	q : (seq Command)-> Time,
	state : State one -> Time
}

noChangeAll にも state の項を追加します。

pred noChangeAll [t, t' : Time, obj : Object] {
	obj.expected.t' = obj.expected.t
	obj.real.t' = obj.real.t
	obj.q.t' = obj.q.t
	obj.state.t' = obj.state.t
}

初期状態を InitDone にします。

pred init [t : Time] {
	all obj : Object | (no obj.q.t and obj.real.t = obj.expected.t and obj.state.t = InitDone)
}

Executing状態の間は assign, copy コマンドが実行できないように pred に事前条件を追加します。加えて、事後の状態をそれぞれAssignAdded, CopyAddedにします。

pred assign [t, t' : Time, obj : Object] {
     no obj' : Object | obj'.state.t = Executing // pre-condition 
     some assign : Assign { 
     	  obj.q.t' = (obj.q.t).add[assign]
	  obj.expected.t' = assign.v
	  noChangeRealValue[t, t', obj]
	  obj.state.t' = AssignAdded
     }
}

pred copy [t, t' : Time, obj : Object] {
     no obj' : Object | obj'.state.t = Executing // pre-condition 
     some cp : Copy { 
     	  obj.q.t' = (obj.q.t).add[cp]
	  obj.expected.t' = cp.src.expected.t
	  noChangeRealValue[t, t', obj]
	  obj.state.t' = CopyAdded
    }
}

次にキューの先頭にあるコマンドをひとつだけ実行する pred を書きます。

pred executeCommand [t, t' : Time, obj : Object] {
     let command = first[obj.q.t] {
		(command in Assign) => (obj.real.t' = command.v and obj.q.t' = rest[obj.q.t] and obj.expected.t' = obj.expected.t)
		(command in Copy) => (obj.real.t' = command.src.real.t and obj.q.t' = rest[obj.q.t] and obj.expected.t' = obj.expected.t)
		(isEmpty[obj.q.t'] => obj.state.t' = ExecuteDone) and (not isEmpty[obj.q.t'] => obj.state.t' = Executing)
	}
}

executeCommand を使うと execute 時にひとつだけコマンドを実行する pred は以下のように書けます。

pred execute [t, t' : Time, obj : Object] {
	some q.t // pre-condition
	no obj : Object | obj.state.t = Executing // pre-condition 
	executeCommand[t, t', obj]
}

execute 時にキューにふたつ以上のコマンドがある場合は、続けて残りのコマンドをする必要があります。それも pred で表します。

pred executeRest [t, t' : Time, obj : Object] {
  	 obj.state.t = Executing // pre-condition
	 executeCommand[t, t', obj]			    	  
}

あとは fact step に executeRest を追加するだけです。

fact step {
	init[to/first[]]
	all t : Time - to/last[] | let t' = to/next[t] |
		one obj : Object |
			(assign[t, t', obj]
			or copy[t, t', obj]
			or execute[t, t', obj]
			or executeRest[t, t', obj])
			and (all obj' : Object | obj' != obj => noChangeAll[t, t', obj'])
}

アサートはstateを使って以下のように書きなおします。

assert RealValueEqualsExpectedAfterExecute {
	all t : Time |
		all obj : Object | 
			obj.state.t = ExecuteDone => obj.real.t = obj.expected.t
}
check RealValueEqualsExpectedAfterExecute for 3 but exactly 1 Object, 4 Time, 4 seq

再びアサートをチェックします。

No counterexample found. Assertion may be valid. 16ms.

オブジェクトがひとつの場合だと反例は見つからないようです。では少しスコープを広げてみます。

check RealValueEqualsExpectedAfterExecute for 3 but exactly 2 Object, 4 Time, 4 seq

すると、

Counterexample found. Assertion is invalid. 62ms.

今度は反例が見つかりました。[Show]で確認すると以下のシーケンスで違反があることが分かりました。

1. 初期状態は、Object0.real = Object0.expected = Zero, Object1.real = Object1.expected = Two
2. Object0.assgin(One). Object0.real = Zero, Object0.expected = One
3. Object1.copy(Object0). Object1.real = Two, Object1.expected = One (= Object0.expected )
4. Object1.execute. Object1.real = Zero, Object1.expected = One

これは、Object1 のキューに入っている copy を実行する前にコピー元となっている Object0 の assgin を実行していないためです。どうやらget前にexecuteするだけでは不十分なようです。

2番目のモデル ー コピー元をexecuteする ー

上記の反例では、コピー時のコピー元の値が期待値と実値で一致していないことが原因だったので、以下のような、copyコマンドをキューに積むときには、コピー元のオブジェクトをexecuteする実装を考えました。

void copy(Object obj)
{
    obj->execute();  // <- コピー元のexecuteを呼ぶ
    add_command(make_command(copy, obj));    
}

fact を使って copy コマンドをキューに積む前に execute するようにします。こうするとcopyコマンドを積む前にexecuteが実行するパスしか検査しません。

fact ExecuteCopySrc {
	all t' : Time - to/first[] | let t = to/prev[t'] |
		all obj : Object | 
			(obj.state.t != CopyAdded && obj.state.t' = CopyAdded) => let command = last[obj.q.t'] {
				((command.src).state.t = ExecuteDone or (command.src).state.t = InitDone)
			}
} 

では検査してみましょう。

assert RealValueEqualsExpectedAfterExecute {
	all t : Time |
		all obj : Object | 
			obj.state.t = ExecuteDone => obj.real.t = obj.expected.t
}
check RealValueEqualsExpectedAfterExecute for 3 but exactly 2 Object, 5 Time, 5 seq

以下のような反例が見つかりました。

1. 初期状態は、Object0.real = Object0.expected = Two, Object1.real = Object1.expected = Zero
2. Object1.copy(Object0). Object1.real = Zero, Object1.expected = Two (= Object0.expected )
3. Object0.assgin(One). Object0.real = Two, Object0.expected = One
4. Object0.execute. Object0.real = One, Object0.expected = One
5. Object1.execute. Object1.real = One, Object1.expected = Two

これは、Object1 のキューに入っている copy を実行する前にコピー元となっている Object0 の値が 3, 4 で Object1 が execute する前に変更されたために起きた違反です。

3番目のモデル ー キューイングするのをひとつずつ ー

上記の反例は、キューに入ったコピー元がそのあとで値を変えてしまうために起きていました。そこで、上記の反例のシーケンスの 2 と 3 の間にも execute する方法を考えました。思いついたのは、新しくコマンドをキューに積むときに、最後にコマンドを積んだオブジェクトを異なる場合はキューに積む前に execute したらどうかというものです。コードにすると以下のような実装です。

void assign(int v)
{
    if (last != this) {
        last->execute(); // <- 最後にキューに積んだオブジェクトのexecuteを呼ぶ
    }
    add_command(make_command(assign, v));
    last = this;
}

そこでこれを fact で表して検証してみました。

pred addCommandAtThatTime [t : Time, obj : Object] {
	let before = to/prev[t] | #(obj.q.before) < #(obj.q.t)
}

fact ExecuteDoneBeforeChangingTarget {
	all disj obj1, obj2 : Object {
		all disj t1, t2 : Time - to/last[] {
			(to/lt[t1, t2] and addCommandAtThatTime[t1, obj1] and addCommandAtThatTime[t2, obj2]) implies {
				obj1.state.t2 = ExecuteDone
			}
		}
	}
}

これで検証すると反例は見つかりません。以下のように

check RealValueEqualsExpectedAfterExecute for 3 but exactly 9 Time, 7 seq

スコープを広げて検査してみましたが、反例が見つからないのでこのモデルは正しそうだと言えます。

おわりに

上記を実装して計測したところなかなかのパフォーマンスだったので以上で設計を終えることにしました。まだまだ改善の余地はありますが、必要十分ということで終えることにしました。

さて、どうだったでしょうか。テストでは自分が思いつくケースしかテストすることはできませんが、Alloyならば（限られたスコープですが）網羅的に検査してくれます。これがテストとモデル検査との大きな違いです。

Alloyの威力が少しでも伝えればいいのですが。

※今回使用したモデルはgithubにあります。
https://github.com/masateruk/blog/tree/master/20111020