Island Life

< Roombaを試してみている。 | 最近、"obsolute" という(多分obsolete... >

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

Past comment(s)

nfunato (2006/10/26 09:57:16):

SPINは、プロトコル検証とか特定の目的には凄く便利だと思いますが、有限の状態を網羅的探索して時相論理式で与えられた命題の真偽を検証するので、プログラムの状態空間をCheckerが処理できる程度の大きさに留めるか、検証したいプログラムを検証したい命題に合わせて余計なところを取り除く(Abstractionする)必要があるんですね。  で、Designing Executable Abstraction(上記のような話)や、これを自動でやろうという試みになります。  NASAのMARS LAND ROVERで Deadlock→WatchdogReset の無限ループになり、JPLでの解析にSPINが役立ったという話は結構 あっち こっちに出ています。  後者は、Lisping at JPL(Erann Gat氏のページ)のThe story of the remote agent bug.からリンクが張られています。Shiroさんの云うLisperかな。   あと、普通の言語じゃないですけど、pi計算に型システムを導入することでdeadlockを判定…みたいなことを東北大の小林先生が研究されていたように思います。

shiro (2006/10/27 01:43:24):

で、御指摘の通りかのLisperはErann Gatです。該当する記事はこれ。 最初の記事がもとで巨大なツリーが出来てて結構読みごたえがあります。