PDD その2

インタフェース誌にPDDのアイディアを書いた[1]。基本的な手順は、

1.      プログラムの目的を事後条件として表す。assert文で表現する。

2.      入力条件を場合分けし、それを事前条件とする。assume文で表現する。

3.      assume文の範囲でコーディングをおこない、検証をパスさせる。

4.      パスさせる過程で反例を分析して、分析結果はコーディングまたは事前条件に反映させる。

5.      残りの入力条件について同様に検証をパスさせる。

6.      全ての入力条件に対して検証が終わったら、事前条件を整理する。

基本的にはプログラムSを下のような形にして、Q∧Ｓ⇒Rを満たす様にする。QとRがプログラムの仕様である。入力条件は実装後はテスト条件として使用できる。

assume(Q);
S;
assert(R);

似たような形をコンピュータのセキュリティ改善に使っている論文があった[2]。この論文ではダイクストラの最弱事前条件を使っている。プログラム検証ツールを使用すれば自動化できる部分もありそうだ。

何もしないスキッププログラムの場合は、S=TrueなのでQ⇒Rになる。プログラム検証ツールは含意論理式の証明器としても使えることが分かったので、[1]ではちょっとした実験を紹介した。この実験を発展させて仕様書検証に使えないか検討してみた。すなわち、VDMで言うところの、陰関数定義をCで書いて検証できれば、仕様検証になる。やってみたら、確かにできそうだが、C言語で事前条件・事後条件を書くのが結構大変である。おかげで、述語論理を使えるVDMや時相論理を使えるモデル検査ツールの便利さが分かった。
モデル検査ツールはテストケースを用意しなくても検証できるが、述語論理式はテストケースが必要になる。と言うことはPDDの過程で作成するテスト条件が述語論理式をC言語で記述するヒントになるのかも知れない。
自然言語から直接Cの様なプログラム言語を書き出すのと、一端、述語論理式を経由するのでは、後者の方が絶対に楽なはずだ。壁の正体は何だろうか?

[1]新・組み込みソフトへの数理的アプローチ（第12回）
テストとプログラム検証――TDD（テスト駆動開発）におけるテスト

[2]B. V. Chess. Improving Computer Security using Extended Static Checking. In Proc of. 2002 IEEE Symposium on Security and Privacy, pages 160-173, 2002.