このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

契約とホーア式をプログラムコードに翻訳する

メイヤー流契約に限らず、一般のホーア式もプログラムコードに翻訳する方法を考えてみました。特に、全称限量子(「すべての…に関して…」を意味する)の扱いを工夫してみます。(これは、「AspectJによる契約駆動開発」に関連したエントリーです。)

明示的な含意記号

契約とホーア式は似てるけどわずかに違う、と言いました。例えば、「事前条件:x > 0、実行文:f(x);、事後条件:result >= 15」の3つ組を考えて:

  • 契約としての解釈:x > 0 が成立しないなら、契約が破られている。
  • ホーア式としての解釈:x > 0 が成立しないなら、この式は真である。

3つ組(トリプル)記法(x > 0){f(x);}(result >= 15) では、どちらか分からないので、契約を (x > 0) && {f(x);}(result >= 15)、ホーア式を (x > 0) ==> {f(x);}(result >= 15) と書き分けるといいかもしれません。ここで「==>」は含意(implicatin; 「ならば」を意味する)記号です。

ブロック内の変数宣言

契約記述に使った特殊な変数resultとかold(式)とかは、一般のホーア式ではうまく使えないので、実行文を書くブロック内に変数を導入するしかないでしょう。

  • {int result; result = getAge();}(result >= 0 && result < 150)
  • {int oldAge; oldAge = getAge(); happyBirthday();}(getAge() == oldAge + 1)

ブロックの内部の構文は、ブロックの内部 ::= 変数宣言* 実行文*となります。個々の実行文は、単なるメソッド呼び出しか、右辺がメソッド呼び出しである代入文です。代入文は変数ごとにたかだか1回です。

代入を伴う等号

スタックに関する条件 (x == top()) ==> {push(y); pop()} (x == top()) を考えると、等式 x == top() を満たすには、 x = top() という代入文を実行してしまうのが早いですね。しかし、事前/事後条件には論理的な条件式以外は書くべきではありません。

妥協案として、x := top() と書くと、「実際には代入文だが、論理的には等式と解釈」だとしましょう。すると、次のような全称記号(forall)と変数は、単なる変数宣言だと思ってかまいません。

  • forall(int x) (x := top()) ==> {push(y); pop();} (x == top())

代入を伴う等号「:=」を使ってもよいのは事前条件のなか、変数に対して1回だけです。

全称限量子と変域

全称記号forallと変数をまとめて、いつでも変数宣言とみなせるわけではありません。先のホーア式内の変数yは、実は全称記号で束縛されます。つまり:

  • forall(int y) forall(int x) (x := top()) ==> {push(y); pop();} (x == top())

このときのyは、(intを32ビットとして)四十億個ほどの値をすべて網羅しなくてはなりません。まー、このケースに限ればできなくもないですが、一般論としては現実的ではありません。

実際には、すべてのint値を調べ尽くさなくても、選び出されたいくつかの値について検証すれば十分でしょう(つうか、そうするしかない)。変数yが実際に走る領域をYとして、全称限量子内に領域(変数の変域)を書き添えます。

  • forall(int y : Y) forall(int x) (x := top()) ==> {push(y); pop();} (x == top())

あれっ、「全称限量子」と「全称記号」という言葉が混じってしまったが同義語です。僕の気分的使い分けは、単なる記号「∀」が全称記号で、「∀x」「∀x:T」とかが限量子。

さて、変数yの変域Yは、実際のテストコードに落とすとき具体化します。


/* セットアップ */
MyStack stk = new MyStack();
// ... stkの状態を調整
/* 変数yの変域を準備 */
int [] Y = {-1, 0, 1, 2};
/* ホーア式に対応するテストコード */
// 全称限量子 forall(int y : Y)
for (int y : Y) {
// 事前条件(検査不要)
int x;
x = stk.top();
// 実行文
stk.push(y);
stk.pop();
// 事後条件
if (! (x == stk.top())) {
throw new Exception("Postcondition Violation");
}
}

一般に、全称限量子は “forall(T v : V)”の形ですが、次の場合は変域Vを省略できます。

  1. 型Tが、簡単に扱える程度の有限個の値しか持たない。例:Tがboolean、byte、enum型。
  2. 変数vが「:=」による等式の左辺となっている。

「型Tの変数vに対する変域V」と全称限量子「forall(T v : V)」という概念は、次のようにコード化されます。


Iterable<T> V;
// Vの初期化
for (T v : V) {
// ...
}

いくつかの変域付き全称限量子を持つホーア式は、次のようなメソッドだと考えられます。


// 真偽を返すなら
boolean constraintIsSatisfied(Iterable<T1> V1, Iterable<T2> V2);

// 違反のとき例外を返すなら
void verifyConstraint(Iterable<T1> V1, Iterable<T2> V2) throws Exception;

Javaに、for-in文、型総称、イテレータなどが入ったので、比較的自然に「述語論理式→プログラムコード」の翻訳が出来るようになりましたね、めでたい