2006/10/26

少し前のIEEE Computer誌にNASAの人が、安全なコードを 書くための10の規則、みたいな記事を書いていたのだけれど、それが普段我々の ようなどっちかというと関数型言語よりのプログラマが考えていることと かなり隔たりがあって興味深かった。以下、主観的要約。 (深く知りたい人は原文をあたってほしい: Gerard J. Holzmann, "The Power of 10: Rules for Developing Safety-Critical Code, Computer 39(6) pp.95--97, June 2006.)

1. 制御フローはシンプルに。gotoやsetjmp/longjmpはもちろん、再帰も禁止。
2. ループを回す回数の上限は静的に決まらないとだめ。
3. mallocは初期化時以外使用禁止。
4. 印刷した時1ページ以上になる関数は書いちゃだめ。
5. 関数のprecondition, postconditionを検査するためのassertionを活用せよ。 関数あたり平均で2個以上。
6. データの宣言される範囲はなるべく小さく。
7. void以外の関数の戻り値は必ず検査せよ。各関数は引数の妥当性を必ず検査せよ。
8. プリプロセッサ(ここではcpp)の使用はファイルのincludeと簡単なマクロに留めよ。 ネストするマクロ展開禁止。トークンの合成禁止。
9. 2レベル以上のポインタの間接参照禁止。typedefでポインタをそうじゃなく見せかけるの 禁止。関数ポインタ禁止。
10. 開発初日から常に、コンパイラの警告レベルを最高にしても警告が出ないようなコードを書け。

1, 2, 3あたりはええええって感じだし、8, 9あたり禁止されると 私なんかはプログラムが書けなくなりそうな気がするんだけど、 これも経験に裏打ちされた話なのだから、こういうのが要求される 世界があるってことでしょう。宇宙とか。

ちなみに1, 2, 3, 9あたりは静的検証ツールを使うことを前提にしていて、 静的検証ツールが追いきれないコードは書くなって意図のようだ。

ところで興味があるのは、コンパイルが通ればバグはまず無い、と豪語するような 強い静的型言語ならこういう条件を言語側でサポートできるかってこと。 少なくとも1, 2, 3あたりは静的に処理量の上限が決まって欲しいってことだから MLやHaskellの型システムだけじゃ検証できないよね。依存型ならできるのかな。

昔、comp.lang.lispあたりで静的型vs動的型のflame合戦が起きた時に、 某毒舌Lisperが、「俺は静的型でバグが潰せるというのはまやかしの安心だと 思っているが、静的検証ツールでバグが潰せるというのは信じている。 マルチタスクのタイミング絡みの非常に微妙なバグを、静的検証ツールで 見つけたことがあるからだ。あれは人間が見つけるのは不可能だ」みたいな 発言をしていた気がする。そう、時間が絡む話も普通の静的型言語は まだ扱わないよね。扱えるのかな。

Tag: Programming