ここ何年か考えているテーマのひとつが「カジュアルなフォーマルメソッド(語義矛盾は承知)」なんですよ。一連の{テスト(Test), 仕様(Specification), 振る舞い(Behaviour/Behavior)}駆動開発なんて動きは、カジュアルなフォーマルメソッドなんだと僕は捉えているわけですが、もう一歩踏み込んで欲しい感じ、隔靴掻痒の不満もあります。
そこでメイヤーに戻って「契約駆動」とか、あるいは「検証駆動」なんて言葉も使ってみたけど、ナントカ駆動には食傷気味。"Offencive Programming"は、「攻撃的プログラミング」と訳されると真意がまったく伝わらないし、、、
紆余曲折の末、「デュアルプログラミング」って言葉を使うことに(暫定的だけど)決めました。そしてエクソシストゲームは、デュアルプログラミングを説明するために案出した“極端化した比喩”です。
内容:
●設計(仕様)と実装
設計(仕様)と実装の関係は、たぶん次のように捉えられることが多いでしょう。
- 仕様は、自然言語や図式を使って書かれる。
- 仕様は、(時間的に)実装に先だって作成される。
これは違うと思うよ。次のように考え直しましょう
- 仕様は、ある種のプログラミング言語で書かれる(べき)。
- 仕様と実装は、どちらが先というわけでもなく、適当に混じり合った順序で作成される。
仕様はプログラミング言語を使って作成されるので、それはプログラムであり、もちろん(適切な実行環境の上で)実行可能(であるべき)です。
仕様を書くこともプログラミングなので、その作業者を設計プログラマ、実装を書くプログラマ(従来の意味のプログラマ)を実装プログラマと呼びましょう。2種類のプログラミング作業、2つの役割があるわけです。(※「設計」という言葉の使い方が不適切かも知れないけど、目くじら立てないでちょうだい。)
●設計プログラミング
仕様を書くこと、つまり設計プログラミングに使う言語は、形式仕様記述言語です。VDM-SLやOBJ*なんてチャントしたのもあるけど、ここではインターフェース+ホーア制約を使いましょう(「今風の型理論入門」参照、ホーア式には明示的含意「==>」を入れている)。
次は、設計プログラム=形式仕様の(毎度お決まりの)例です。
spec IntStack {
interface {
new(); // コンストラクタ仕様も記述できるとする// @Accessorは副作用がないことを意味する
@Accessor
int top();
@Accessor;
boolean isEmpty();void push(int x);
void pop();
}// 制約[1]に関しては、後に説明あり
[1] forall(int x) (isEmpty()) ==> {push(x);} (!isEmpty());
[2] // ...
// ... 以下省略
}
設計プログラマは、なんらかの意図や構想を心に持っています。その意図/構想を設計プログラミング言語=形式仕様記述言語によって書き下します。それが、設計プログラミングの作業ですね。
●悪魔の実装プログラマ
さて、実装者として悪魔を登場させましょう。彼は悪魔なので、設計プログラマの意図/構想は完全にお見通しです。彼は悪魔なので、設計プログラマの意図/構想を知った上で、わざと意図/構想と違う実装をします。例えば、IntStackのインターフェースだけが提示された段階では次の実装をします。
public class DemonicIntStackImpl_0 implements IntStack {
public DemonicIntStackImpl_0() {}public int top() {return 0;}
public boolean isEmpty() {return true;}public void push(int x){}
public void pop(){}
}
ただし、この悪魔はけっこう素直な奴で、インターフェースが提示されれば、それをimplementsするし、(形式的)制約が課せられれば、それを遵守します。でも悪魔ですからね、インターフェースや制約に記述されてないことに関しては、ことごとく設計プログラマの意に反することをやらかします。
●意地悪だが素直な奴
とりあえず、forall(int x) (isEmpty()) ==> {push(x);} (!isEmpty());
という制約を考えてみると、これは:
を意味します。
どんな整数xに対しても
事前に isEmpty() ならば
push(x); を実行すれば
その事後は、!isEmpty() である。
素直な悪魔は制約には従うので、実装を次のように変更します。
public class DemonicIntStackImpl_1 implements IntStack {
public DemonicIntStackImpl_1() {}public int top() {return 0;}
public boolean isEmpty() {return false;}public void push(int x){}
public void pop(){}
}
これで制約[1]を満足するかって? 制約[1]には「事前に isEmpty() ならば」という条件が付いているので、この事前条件が成立しないときは何も問われない、つまりOKなのです。isEmpty()は常にfalseを返すので、制約[1]は常に満足されます。
●悪魔を追いつめる悪さ封じの呪文
ここらへんで、設計プログラマをエクソシスト(悪魔払いの祈祷師)と呼び替えます。形式仕様記述の制約は、悪魔が悪さするのを封じる呪文なのです。どんどん呪文を積み重ねて、悪魔が悪さをする余地をなくすのがエクソシストの仕事です。
次の呪文を追加しましょう。
[2] {new();} (isEmpty())
ここで、コンストラクタを意味するnewだけは特別扱いで、何もない(当該オブジェクトも存在しない)ところで実行し、実行後にできたオブジェクトに対して事後条件をチェックします。と、そうすると、常にfalseを返すisEmpty()は封じられます。
念のため言っておくと、次の実装を悪魔が採用することはできません。
public class DemonicIntStackImpl_2 implements IntStack {
private boolean justCreated;public DemonicIntStackImpl_2() {
justCreated = true;
}public int top() {return 0;}
public boolean isEmpty() {
if (justCreated) {
justCreated = false;
return true;
} else {
return false;
}
}public void push(int x){}
public void pop(){}
}
なぜなら、isEmpty()はアクセッサだと指定されているので、二度続けて呼ばれたときに違う値を返すことはできないのです。
悪魔は、こうくるでしょ:
public class DemonicIntStackImpl_3 implements IntStack {
private boolean empty;public DemonicIntStackImpl_3() {
empty = true;
}public int top() {return 0;}
public boolean isEmpty() {return empty;}public void push(int x){empty = false;}
public void pop(){}
}
●戦いは続く
エクソシストは次の呪文を投入します。
[3] forall(int x) {push(x);} (top() == x);
これで、pushの引数を捨てるわけにはいかなくなります。もちろん悪魔は、pushの引数を保存する変数private int lastPushed;
で対応します。エクソシストは追い打ちをかけます。「俺のターン」:
[4] forall(int y, x) (top() == x) ==> {push(y); pop();} (top() == x);
おー、これは効果的だぁー。悪魔も苦しくなってきたぞー。
●エクソシストゲームからデュアルプログラミングへ
と、まー、こんな感じで進むのがエクソシストゲームです。エクソシスト=設計プログラマは、悪さを封じる呪文=形式仕様記述を駆使して悪魔と戦います。
この戦いはいつまで続くのでしょうか。エスソシスト=設計プログラマが、自分の意図/構想を仕様(呪文の積み重ね)として完全に表現し尽くしたと思ったとき、そして悪魔の実装プログラマがその仕様に対してvalidとなる実装プログラムを書いたとき、それが戦いの終わりです。
ここで、悪魔とエクソシストという2つの役割が登場しています。また、設計プログラミングと実装プログラミングという2種類のプログラミングも出てきてますね。これら、対立するようで相互補完しあう2者にちなんでデュアルプログラミングと名付けました。
実は、デュアルと呼ぶ理由はもうひとつあり、仕様と実装が実際に双対性(duality;そうついせい or そうたいせい)を持ち、双対性を支える構造が確実に存在するからです。この構造により、設計プログラムの“実行”が可能となります。このへんのハナシはデュアルプログラミングの続編にします、また、いずれ。