非決定性写像の圏におけるホーア式のモデルいちおう完結・編

続き＆完結。

内容：

アブラムスキー達の仕様構造
メイヤーのCommandとQuery（教えに背く）
メイヤーの契約（教えを省く）
エクスペクテーション
エクスペクテーションの実行
エクスペクテーション・ベースのホーア式
純粋なホーア式とエクスペクテーション
FITスタイルの記述
インタープリタとエクスペクテーション
最後に

全体：

アブラムスキー達の仕様構造

ここらで、仕様構造（specification structure）に触れておきます。仕様構造は、プログラムの実行を圏でモデル化したとき、ホーア論理をどう定式化すべきかの一般的な処方箋を与えます。ネタ元は例えば：

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.6943
"Specification Structures and Propositions-as-Types for Concurrency" (1995) Samson Abramsky, Simon Gay, Rajagopal Nagarajan

これまでに説明した、「非決定性写像の圏NDMap ＋ブール代数の集まり」は、仕様構造の一例になっています。とりあえず圏C上の仕様構造の定義を天下りに述べます。

圏C上の仕様構造を構成する素材は、次のものです。

圏Cの各対象Xに対して、集合P(X)が割り当てられている。
圏Cの各対象X, yに対して、P(X)×C(X, Y)×P(X)の部分集合H(X, Y)が割り当てられている。

P(X)は、X上のpropertyの集合と呼ぶようです。H(X, Y)は、「Xのproperty、XからYへの射、Yのproperty」の間の三項関係だと言えます。文字'H'を使っているのは、H(X, Y)がホーア（Hoare）トリプルの集合とみなせるからです*1。

それで仕様構造の公理ですが、次の2つです。

p∈P(X) のとき、(p, id_X, p)∈H(X, X)
p∈P(X), f:X→Y, q∈P(Y), g:Y→Z, r∈P(Z) のとき、(p, f, q)∈H(X, Y) かつ (q, g, r)∈H(Y, Z) ならば、(p, f;g, r)∈H(X, Z)。

この一般的な定義を「非決定性写像の圏NDMap ＋ブール代数の集まり」に場合に当てはめてみます。まず、対象S上のpropertyの集合は、条件の集合Ω(S)のことです。次に対象S, Tに対してホーアトリプルの集合H(S, T)を定義するのですが、それは次のようにします。

p∈Ω(S), f:S→T, q∈Ω(Y) のとき、(p, f, q)∈H(X, Y) ⇔ p・f = p・f・q

p・f = p・f・q という等式は、ホーアトリプル（ホーア式）が正しいことを主張する等式でした。つまり、H(S, T)は正しい（成立する）ホーアトリプルの集合になります。このΩとHに関して、仕様構造の公理が成立することは等式計算で直接確認できます。

また、仕様構造の公理は、最小ホーア論理の「空文の公理（skipの公理）」と「順次結合の推論規則」に対応しています。つまり、仕様構造とは、演繹系である最小ホーア論理の圏論的モデルとしてピッタリの構造なのです。ベースとなる圏に、より豊かな構造（クリーネスターとかトレースとか）を入れれば、より精密なモデルが構成可能です。

アブラムスキー達の論文では、圏Cに仕様構造Sが付随しているとき、新しい圏C_Sが作れることが書いてあります。「非決定性写像の圏NDMap ＋ブール代数の集まり」の場合、この方法を使って構成した圏は、NDMapのカロウビ展開圏とほとんど同じ（完全に同じではない）になります。なんでそうなるかというと、「条件（述語、性質）、部分集合、ヴァリデータ、ベキ等射、EPペア」などがよく似た概念なので、条件をもとに作った拡張圏も、ベキ等射をもとに作った拡張圏も似たりよったりということです。

メイヤーのCommandとQuery（教えに背く）

バートランド・メイヤーは、2種類の望ましいメソッド種別を提唱しています。オブジェクト指向のクラスを、状態空間Sとその上の写像としてモデル化します。オブジェクトのある時点での状態は、Sの一点で表現され、オブジェクトの振る舞いはS上の運動（通常は離散時間）の軌跡になります*2。

状態遷移（オブジェクトの状態空間内の運動）を引き起こすメソッドをメイヤーはCommandメソッドと呼びます。これは、非決定性写像 f:S→S で表現できます。Commandメソッドに引数があるなら、引数値の集合をXとして、S×X→S となります。Commandメソッドに戻り値はありません。副作用（主作用ですけど）があるだけです。

一方、状態空間S上で定義された関数をQueryメソッドと呼びます。関数＝Queryメソッドは戻り値を持つので、戻り値の集合をYとすると、S→Y という写像（非決定性じゃなくて普通の写像）です。引数を持つQueryメソッドなら、S×X→Y 。Queryメソッドは状態遷移（副作用）を引き起こしません。

メイヤーは、戻り値も副作用も両方持つようなメソッドは使わないで、CommandメソッドとQueryメソッドだけでインターフェースを設計したほうがいいよ、と言っています。しかし現実には、戻り値と副作用（状態遷移）の両方を持つようなメソッドもあります。そのようなCommand-Query混合型のメソッドは、S×X→S×Y と表現できます。S×X→S がCommandのパート、S×X→Y がQueryのパートです。例外を引き起こす可能性があるなら、Yを正常値Nと例外値Eに分けて、S×X→S×(N + E) とします。状態と例外を含むプログラムの計算は、「シーケント計算と例外処理コード」と「色付き絵算と分合律」を参照してください。

メイヤーの契約（教えを省く）

もうひとつメイヤー先生ご謹製の概念・手法に契約があります。メソッドを f:S×X→S×Y だとすると、fの契約とは、p∈Ω(S×X), q∈Ω(S×Y) という条件のペアのことです。fとp, q から三つ組(p, f, q)を作ると、ホーア式（ホーアトリプル）と区別が付きませんが、契約とホーア式は異なります。事前条件pが不成立のとき、契約では失敗（契約違反）と考えますが、ホーア式では成功です。

事前条件が常に成功するような条件（いつでも値がtrue）だとすると、契約とホーア式の差がなくなります。そもそも、三つ組の必要がなくて、ペア(f, q)で十分です。このペアは、事後条件だけが付いたメソッドだといえます。

エクスペクテーション

f:S×X→S×Y が戻り値も副作用も持つ可能性があるメソッドだとして、fに関するエクスペクテーションとは、(s, x, f, q) という四つ組のことです。それぞれの意味は以下のとおりです。

sは状態空間Sの一点。
xは引数の集合Xの要素。
fはメソッド（のモデルである非決定性写像）
qはS×Y上で定義された決定性の二値ブール値関数

このなかで、状態点sは実行環境により暗黙に与えられるとすると、三つ組(x, f, q)でエクスペクテーションを表現してもいいでしょう。xはfへの引数（明示的な入力）、qは事後状態と戻り値（例外も含まれる）に関する条件です。ほとんどの場合、qは戻り値だけをチェックしますが、たまに事後状態を調べる必要もあります。

ここで、(f, q)は契約の事後条件（Eiffelならensure）だけを伴ったメソッドです。つまり、エクスペクテーション(x, f, q)は、半分契約付きのメソッド(f, q)に、特定の引数xを指定したものです。引数が不要のときは、nilとかnullとかundefinedとか、なんか適当な目印を付けておきます。特定の状態sも指定されるのですが、これは通常、別なタイミングでセットアップされているとします。

エクスペクテーションの実行

エクスペクテーション(s, x, f, q)を実行するとは、「特定の状態sで、特定の引数xをfに渡して実行し、事後にqによる検査を行う」ことです。qによる検査結果が真なら成功、偽なら失敗といいます。

先に述べたように、状態点sは前もってセットアップされていると想定して、エクスペクテーションを(x, f, q)と書くことにします。さらに、e = (x, f, q) とか e₁ = (x₁, f₁, q₁) のような書き方もします。

エクスペクテーションの列 [e₁, e₂, ..., e_n] に対して、この列の実行（通常実行）とは、e₁から順番に逐次実行することです。ただし、どこかで失敗すると、それ以上は実行しません。エクスペクテーションの列の強制実行とは、途中で失敗してもかまわずに最後まで実行してしまうことです。特別なケースとして、空列 [] を実行するとは、何もしないでただちに成功とすることです。

通常実行でも強制実行でも、すべてのエクスペクテーションが成功すれば列の実行も成功です。エクスペクテーションが1つでも失敗すれば、列の実行は失敗です。成功と失敗の判定には、通常実行であるか強制実行であるかは関係しないことに注意してください。通常実行と強制実行の区別や用途は、実用上の要求で決まってきます*3。

エクスペクテーションの列 [e₁, e₂, ..., e_n] の実行ログとは、それぞれのエクスペクテーション実行により得られた事後状態s'、戻り値y、成功・失敗の別rの組(s', y, r)を並べたものです*4。列の実行が成功するか、または強制実行であった場合は、もとの列と同じ長さの実行ログが得られます。通常実行の場合は、もとの列よりも短い実行ログのことがあります。実用の観点からは、実行ログが最も重要な成果物となります。

エクスペクテーション・ベースのホーア式

前節で、エクスペクテーションの列 [e₁, e₂, ..., e_n] に対して、その実行と成功・失敗を定義しました。エクスペクテーション列を3つ組にした、([p₁, ..., p_k], [e₁, ..., e_n], [q₁, ..., q_m]) を、エクスペクテーション・ベースのホーア式（ホーアトリプル）と呼ぶことにします。トリプルのなかに空列を含んでもかまいません。全部空列であっても問題はありませんが、現実的な都合から真ん中は空でないとしておきます。

さて、エクスペクテーション・ベースのホーア式に対しても、その実行と成功・失敗を定義します。

[p₁, ..., p_k] の実行が失敗した場合は、ホーア式の実行は成功である。
[p₁, ..., p_k] の実行が成功した場合は、次に進む。
[e₁, ..., e_n] の実行が失敗した場合は、ホーア式の実行は失敗である。
[e₁, ..., e_n] の実行が成功した場合は、次に進む。
[q₁, ..., q_m] の実行が失敗した場合は、ホーア式の実行は失敗である。
[q₁, ..., q_m] の実行が成功した場合は、ホーア式の実行は成功である。

純粋なホーア式とエクスペクテーション

エクスペクテーション・ベースのホーア式では、条件と実行文の区別がなくなっています。このため、条件の評価が副作用を引き起こす可能性があります。また、実行文にも真偽（成功・失敗）があるので、事後条件に至る前に失敗の判定が下されたりします。

これは、本来のホーア式／ホーア論理をかなり変形していることになります。そうなると、本来のホーア式／ホーア論理をどのくらい変形したのか（差分）をハッキリとさせる必要があります。ホーア論理を無茶苦茶にしてしまったのではないか？似ても似つかないゲテモノを作ってしまったのではないか？という懸念があるからです。

僕としては、本来のホーア論理を極力保存しようと気を使いました。実際に「保存」されていることを保証するには、次のことを示す必要があります。

本来のホーア論理の構文と意味論が、エクスペクテーション・ベースのホーア論理のなかに埋め込める。

これが成り立たないとなると、「ホーア論理を無茶苦茶にしてしまった、似ても似つかないゲテモノを作ってしまった」と言われてもしょうがないでしょう。無茶苦茶なゲテモノでは、ホーア論理に関する多くの理論や手法が使えなくなってしまいます。

ところで、上の命題を示すとは言っても、「本来のホーア論理の構文と意味論」とか「埋め込める」とかの意味が明らかでないと何もできません。今まで、（本来の）ホーア論理がどういうものであるかを述べてきたのは、上記の命題をハッキリとさせるためです。ホーア論理の定式化はいくつもありますが、非決定性写像の圏NDMapにブール代数の仕様構造(Ω, H)を載せたものは計算しやすいと思います*5。

今まで述べた定義を使えば、（本来の）ホーア論理の条件や実行文をエクスペクテーションとして表現することは容易でしょう。構文と意味を、順次翻訳していくこともそれほど難しくはないと思います。その埋め込みの細部は退屈なんで、今日はやめておきます。

FITスタイルの記述

αをホーア式として、αが特定のモデルMに対して妥当であることは、M |= α と書けます。「非決定性写像の圏におけるホーア式のモデル踊り場・編」に書いたように、モデルとしては、状態空間Sの点s（あるいは s:1→S）を採用しますから、s |= α となります。αがエクスペクテーションベースのホーア式であっても同様に考えます。

αは3つの部分 p, f, q から構成されるので、全体は s, p, f, q のパーツから構成されます。これを次のレイアウトで示しましょう。



  状態sの指定 ＝ セットアップ部

    …

    …

  ホーア式αの指定

    事前条件pの指定（省略可能）

      … 

    実行文fの指定

      … 

    事後条件qの指定（省略可能）

      …

このスタイルが基本ホーアテスト s |= α の記述となります。より一般的なホーアテスト、例えば s, t |= α, β, γ のレイアウトもこれに準じます。

ホーア式αを構成する p, f, q は、それぞれエクスペクテーションの列となります。各エクスペクテーションを“表（テーブル）の1行”として、エクスペクテーション列全体を表形式にするのが、カニンガムのFITのアイディアです（ただし、カニンガムはホーア式を導入していません）。さらにFitNesseでは、テキストで手書きが容易なようにWiki記法を採用しています。

インタープリタとエクスペクテーション

カニンガムのFITでは、表（テーブル）によるエクスペクテーション（上で僕が定義したエクスペクテーションと一致するとは限らない）の記述とソフトウェア内部を結びつけるために、フィックスチャと呼ばれるプログラムが必要になります。僕は、フィックスチャの必要性がFITの最大の難点だと思っています。

Catyでは、フィックスチャは不要です。なぜかというと、Catyは本質的にインタープリタだからです。ソフトウェアシステムの提供するすべての機能に、インタプリタ経由でアクセスできます。つまり、インタプリタ（コマンドラインシェル）を使って何でも調べることができるのです。

Catyにおいて、人間が手作業・目視でテストするときは、コマンドラインを手で書いて、出力結果を目で見て判断という作業を繰り返します。必要に応じてファイルを作ったり、ファイルの中身を覗いてみたりもします。1行のコマンドラインとその出力の目視判断を記述したのがエクスペクテーションに他なりません。一連のコマンドライン投入＆確認作業は、エクスペクテーションの列 [e₁, ..., e_n] に対応します。

「(1)テストにふさわしい状況を作り出すセットアップ作業（使う道具は主にテキストエディタ）、(2)テストの前提が満たされているかの確認、(3)一連のコマンドライン投入、(4)実行の効果の確認」が、それぞれ、「(1)状態s, (2)事前条件p、(3)実行文f, (4)事後条件q」に対応しています。さらに、読み書きの容易さを考慮して、それらがWiki記法の見出しや表（テーブル）の構文を借用して記述できるわけです。一度書いたホーアテストの記述（振る舞い、あるいは仕様の記述）は、何度でも繰り返し自動実行できます。

Caty特有の事情から話が簡単になっているのは否定できませんが、インタプリタがシステムのインターフェースになっているなら、フィックスチャなしのFITが使える可能性は高いと思います。

最後に

とりあえず、大急ぎでエクスペクテーション・ベースのホーア論理というものを説明しました。本来のホーア論理の拡張になっていますが、条件（論理式）と実行文（プログラム手続きコード）の区別がないので、ある意味では不純というか汚い拡張です。しかし、本来のホーア論理をこのなかに埋め込めるので、副作用・戻り値のあるなしを自分で注意すれば*6、本来のホーア論理の部分的検証系としても使えます。

条件と実行文の区別をやめたのは、「あまり綺麗事も言ってられない」という実用上の理由です。細部を、いや細部じゃない肝心なところ（例えば、本来のホーア論理をエクスペクテーション・ホーア論理に埋め込むとか）を端折ってるし、実例がほとんどないのですが、実例は今後紹介する機会はきっとあると思いますので、この話はこれでいちおうの完結とします。

*1:アブラムスキー達の論文では文字'R'（Relation）が使われています。

*2:オブジェクト指向と関係なくても、プログラムの振る舞いをモデル化すると、だいたいこうなります。

*3:理論上は、この区別は不要です。区別すると鬱陶しいことになります。

*4:実際には、状態を完全に記録するのは困難です。ここは概念的な話です。

*5:デクスター・コォゼンのテスト付きクリーネ代数（KAT）もなかなか良いですが、仕様構造を使う方が僕の好みです。コォゼンのKAT方式： http://www.cs.cornell.edu/~kozen/papers/Hoare.pdf

*6:ここは残念なところですが、エクスペクテーションとホーア論理を整合させるために致し方ないのです。