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

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

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

参照用 記事

デュアルプログラミングとエクソシストゲーム

ここ何年か考えているテーマのひとつが「カジュアルなフォーマルメソッド(語義矛盾は承知)」なんですよ。一連の{テスト(Test), 仕様(Specification), 振る舞い(Behaviour/Behavior)}駆動開発なんて動きは、カジュアルなフォーマルメソッドなんだと僕は捉えているわけですが、もう一歩踏み込んで欲しい感じ、隔靴掻痒の不満もあります。

そこでメイヤーに戻って「契約駆動」とか、あるいは「検証駆動」なんて言葉も使ってみたけど、ナントカ駆動には食傷気味。"Offencive Programming"は、「攻撃的プログラミング」と訳されると真意がまったく伝わらないし、、、

紆余曲折の末、「デュアルプログラミング」って言葉を使うことに(暫定的だけど)決めました。そしてエクソシストゲームは、デュアルプログラミングを説明するために案出した“極端化した比喩”です。

内容:

  1. 設計(仕様)と実装
  2. 設計プログラミング
  3. 悪魔の実プログラマ
  4. 意地悪だが素直な奴
  5. 悪魔を追いつめる悪さ封じの呪文
  6. 戦いは続く
  7. エクソシストゲームからデュアルプログラミングへ

●設計(仕様)と実装

設計(仕様)と実装の関係は、たぶん次のように捉えられることが多いでしょう。

  • 仕様は、自然言語や図式を使って書かれる。
  • 仕様は、(時間的に)実装に先だって作成される。

これは違うと思うよ。次のように考え直しましょう

  • 仕様は、ある種のプログラミング言語で書かれる(べき)。
  • 仕様と実装は、どちらが先というわけでもなく、適当に混じり合った順序で作成される。

仕様はプログラミング言語を使って作成されるので、それはプログラムであり、もちろん(適切な実行環境の上で)実行可能(であるべき)です。

仕様を書くこともプログラミングなので、その作業者を設計プログラマ、実装を書くプログラマ(従来の意味のプログラマ)を実装プログラマと呼びましょう。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 そうたいせい)を持ち、双対性を支える構造が確実に存在するからです。この構造により、設計プログラムの“実行”が可能となります。このへんのハナシはデュアルプログラミングの続編にします、また、いずれ。