最近Alloyで集中的に作業する機会があり、仕様記述におけるよくある落とし穴について考えるようになりました。本文で述べることはあらゆる形式仕様に当てはまります。折りたたみの中は、Alloy上級者向けの補足です。

シンプルな依存関係ツリーのモデルを考えてみましょう。プログラムにはトップレベルの依存関係があり、それぞれがさらに依存関係を持つ、といったものです。Alloyでは次のようにモデル化できます。

sig Package {
  , depends_on: set Package
}

run {some depends_on}

abstract sig Package {
  , depends_on: set Package
}

lone sig A, B extends Package {}

run {some depends_on}

生成された例をいくつか見てみると、奇妙なことに気づきます。なんと、パッケージが自分自身に依存しているのです！

仕様を書いていると、このようなナンセンスな状況はよく起こります。システムがどうあるべきかという意図はあるのに、それを明示的にエンコードしていないためです。そうした事態を防ぐために、追加の制約を加える必要があります。そのために、Alloyには特別な「fact」キーワードが用意されています。¹

fact no_self_deps {
    all p: Package {
       p not in p.depends_on 
    }
}

fact {
    no depends_on & iden
}

Alloyはfactに違反するモデルを一切生成しませんし、そうしたモデルにおいて不変条件の違反を探すこともありません。factは「現実の事実」であり、そもそも探索する必要がないものとして扱われるのです。

factの落とし穴

「自己依存なし」は、factのわかりやすい例です。同時に、ひどいfactの例でもあります。初心者は、システムをモデル化するためにfactを使いがちですが、これはすぐに問題を引き起こします。

仕様ではなく、実際のシステムについて少し考えてみましょう。パッケージマネージャーの依存関係はどこから来るでしょうか。通常はpackage.jsonやCargo.tomlのようなプレーンテキストファイルです。もし誰かが手作業でそのファイルに自己依存を書き込んだらどうなるでしょうか。おそらく、パッケージマネージャーにはその自己依存を検出してエラーとして入力を拒否してほしいはずです。そのエラーハンドリングが正しく動くことを、どうやって確認するのでしょうか。チェッカーに、有効なマニフェストは受け入れ、自己ループを含むものは拒否することを検証させるのです。

しかし、自己依存を一切生成しないようにfactで指示してしまったため、その拒否をテストできません。factによって、自己依存が「表現不可能」になってしまったのです。

通常、プログラミング言語において「不正な状態を表現不可能にする」（MISU）は良いこととされています（1 2 3 4）。しかし仕様は、あなたが書いているソフトウェアだけでなく、それが動作する環境、すなわち機械と世界（the machine and the world）の両方をカバーします。不正な状態を表現できなければ、世界が不正な状態を作り出し、それをソフトウェアが処理しなければならないという状況自体を表現できないのです。

factの代わりに使いたいのが述語（predicate）です。そうすれば、述語が真である場合をテストしたり、他の性質を得るためにその述語が必要であることを検証したりできます。制約を暗黙的ではなく明示的にするのです。

// instead of

fact no_self_deps {/*body*/}

run {some_case}
check {some_property}

// do

pred no_cycles {/*body*/}

run {
  no_cycles and some_case
}

check {no_cycles implies some_property}

述語には、「局所的にスコープされる」という追加の利点もあります。3つのfactがあるときにそのうち2つだけを使ってモデルをチェックしたい場合、3つ目のfactをコメントアウトしなければなりません。

factを使うべきとき

では、どこでfactを使うべきなのでしょうか。モデルを弱める可能性があるにもかかわらず、制約を普遍的に課すことが理にかなうのはどんなときでしょうか。

第一に、factは問題のスコープを絞るのに役立ちます。「自己依存なし」は、私たちがパッケージインストーラーだけを仕様化しており、マニフェストの検証は別の何かが担当する場合であれば、まったく妥当なfactです。これをfactとして書くことで、読者に対してマニフェストの検証は対象外であることが明確になります。これは、もしその仮定が偽であった場合、私たちは何の保証もしないということを意味します。

第二に、factは根本的につまらないケースを除外します。たとえば、連結リストをモデル化するとします。

sig Node {
  next: lone Node //lone: 0 or 1
}

これは通常のリストと循環のあるリストの両方を生成しますが、どちらも私にとっては興味深いケースです。どちらも制約で除外したくはありません。しかし同時に、互いに素な2つのリストを持つモデルも生成されます。単一の連結リストだけに関心があるのであれば、factで余分なリストを除外できます。

fact one_list {
    some root: Node | root.*next = Node
}

open util/graph[Node]

fact {
    weaklyConnected[next]
}

同様に、余計な詳細を省くためにfactを使うこともできます。ユーザーとグループをモデル化する場合、空のグループは不要です。その場合はUsers.groups = Groupのようなfactを追加します。

第三に、制約を使って遅いモデルを最適化できます。これは通常、対称性の破れによるものです。

最後に、Alloyがネイティブに表現できない必要な関係を定義するためにfactを使うことがあります。私が携わったプロジェクトでは、グラフにRedノードとBlueノードがありました。Redノードは他のノードへ少なくとも1つのエッジを持ち、Blueノードは高々1つのエッジを持ちます。当初は次のように書いていました。

abstract sig Node {
}

sig Red extends Node {
  edge: some Node
}

sig Blue extends Node {
  edge: lone Node
}

しかし、これではedgeを使う汎用的な述語をノードについて書くことができませんでした。Alloyがそれを型エラーとして扱うためです。そこで、代わりにfactを使って次のように書き直しました。

abstract sig Node {
  edge: set Node
}

sig Blue, Red extends Node {}

fact {
  all r: Red  | some r.edge
  all r: Blue | lone r.edge
}

module main

// spec

check {spec => always (prop1)}
check {spec => always (prop2)}

// etc

open main

fact {spec}

check {always (prop1)}
check {always (prop2)}
// etc

結論

制約は危険です。なぜなら、プログラムがエラー状態を回避することを検証するには、そもそもエラー状態自体が必要だからです。

Alloyについてもっと学びたい方は、こちらの良書や、私がメンテナンスしているリファレンスドキュメントが参考になります。現在、新しいAlloyワークショップも準備中です。先月アルファテストを実施し、今夏の後半にベータテストを予定しています。最新情報を入手するには、私のニュースレターにご登録ください！

Jay Parlar氏とLorin Hochstein氏にフィードバックをいただきました。この記事を気に入っていただけたなら、ぜひニュースレターにご参加ください！毎週新しいエッセイを書いています。

私は企業向けに形式手法のトレーニングを行い、ソフトウェア開発をより速く、より安く、より安全にしています。詳細はこちらをご覧ください。

1. 他の仕様記述言語では、これは通常、実行時制約（TLA+のように）か、システム仕様自体への直接的な変更のいずれかです。[return]