バグのないプログラムを作るための技術
2015/12/10 追記: バグを本気で無くしたい方はこんな良く辺鄙なブログなんて見ずにソフトウェアエンジニアリング系の国際学会に行くなり、そこの論文を読むなりするといいと思います。ICSEなんかは日本語の勉強会資料もあってとっつきやすいでしょう。
バグのないプログラムを作る方法について色々聞きかじったことを, 脈絡なく訳の分からない説明でつらつらと書きならべます.
テスト
割と古典的な方法ですね. プログラミングコンテストでもお馴染みの方式です. Java だと JUnit (4) みたいなのを使います.
- 手作りケース
- とりあえず試してみるケース
- コーナーケース
- ミスの発生しやすそうなところを突くためのケース
- ランダムケース
- ランダムに爆撃するためのケース
みたいなものを作って, 仕様とマッチするか確認します.
当たり前ですが, 基本的には下手な鉄砲も数撃ちゃ当たる方式なので, 運が悪いとバグがあっても見つかりません. あと, ランダムではまずコーナーケースは生成されないので, 他の方法で作る必要があるのですが, ちゃんとしたコーナーケースを揃えるのが難しい場合もあります.
モデル検査
時相論理などに基づいた手法です. プログラムの記述するシステムを考え, その状態空間を探索して, 始状態からエラー状態にたどり着かないかを確認します. Java だと Java Path Finder (4 or 6) みたいなのを使います.
テストに比べると無駄なく系統的にすべての場合を調べつくせるので, バグのないことを証明しやすいのですが, 当然ながら状態爆発で, あまり複雑なプログラムには使えません. 複雑なプログラムにこそ欲しいのに...
頑張って状態数を減らすことが必要で, そうするとシステムについて深く考察しなければならないので, プログラムを証明するより手間が大幅に削減されているとは言いがたい気がします.
でも, 高信頼性の必要なプロジェクトで色々使われているみたいです. あと, 並列処理にはいい感じみたいです.
証明からのプログラム抽出
プログラムの証明には Hoare 論理などが使われますが, せっかく証明を書いても普通のコンパイラはそれを処理することができないので, 証明は Coq などの定理証明支援系で処理できる形で書くことが多いようです. 証明とプログラムが離れていると問題なので, そのままプログラムを出力してしまうということまでやられているようです.
状態は爆発しないのですが, やはり面倒ですね.
プログラムの大きさに応じて, モデル検査と併用して使うプロジェクトがいくつかあるようです.
運算
複雑なプログラムを書くと, どうしてもバグを減らしたり, 証明したりするのが面倒になります. なので, 最初は効率は特に考えず, 単純な(良型の)プログラムを書き, 等価変換規則を順に適用して, 目的のスペックを持つプログラムを導いてしまおうという方針があります. この方針では, やはり仕様も証明などという別の形式ではなく, プログラムで書けたほうが素晴らしいですよね,
ということになります.
参考書はこれ: http://www.amazon.co.jp/dp/013507245X
しかし, 変換規則の適用順序はあまり自明でないので, 人間の知恵に頼って変換するしかないのが実情です. それもまだ範囲があまり広くはないという...
という訳で, 基本的には, 最初から最適化を当てにして単純なプログラムを書くものではなくて, 既に動いているプログラムの高速化を図る手段なわけです. GHC の最適化の一部として成果がいくらか採用されています.
型検査
各データに対して, できる処理を宣言し, 制限をかけることによって, ナンセンスな処理を行うプログラムを弾く方法です.
オブジェクト指向的なアレとも言えます. もっとも検査がいい加減な処理系では意味がありませんが.
構文検査で文法的に何語か分からないプログラムを弾いて, 型検査で文法的に正しいけれども意味の分からないものを弾くわけですね. こうしてつまらないバグを消します.
でも, 型を真面目に書くのは面倒です. なので, 型推論がついていると嬉しいのですが, さすがに行列のサイズを確認したり,
配列の長さを確認したり, ということができるというものまでは,
あまり一般的ではないようです. 破壊的に書き換えられる型が存在するとややこしくなるせいなのか, 命令的なものにはあまりついてませんよね.
あと, プログラムの型と言っても2系統あります.
オーバーロードは基本的に下の発想に基づいているので, それを引きずった仕様を採用している言語では, 役に立たないかも知れません. Haskell なんかでは, 型推論の関係上, 下みたいな使い方は虐げられている感じです.
まとめ
| 手法 | 仕様の記述法 | 検査される仕様 | 大規模化 |
|---|---|---|---|
| テスト | 正解入出力データ, 検証プログラムなど | 一部 | ○ |
| モデル検査 | プログラムのモデル, assert文の埋め込みなど | 全体 | × |
| 証明からの抽出 | 証明 | 全体 | ○ |
| 運算 | 愚直なプログラム | 全体 | ○ |
| 型検査 | 型 | 一部 | ○ |
おまけ
こんな話 http://twitter.com/#!/xyx_is/status/139344395748122625 もありますけど, プログラムには計算量の観点から"手順"などの追加情報が入っているので, これを忘れた世界で考えて, 自然言語で記述される仕様との乖離を評価しやすくしようというのが, この手の話の趣旨だと思います. でもやはり差は残ってしまうものですね.
