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.)
- 制御フローはシンプルに。gotoやsetjmp/longjmpはもちろん、再帰も禁止。
- ループを回す回数の上限は静的に決まらないとだめ。
- mallocは初期化時以外使用禁止。
- 印刷した時1ページ以上になる関数は書いちゃだめ。
- 関数のprecondition, postconditionを検査するためのassertionを活用せよ。 関数あたり平均で2個以上。
- データの宣言される範囲はなるべく小さく。
- void以外の関数の戻り値は必ず検査せよ。各関数は引数の妥当性を必ず検査せよ。
- プリプロセッサ(ここではcpp)の使用はファイルのincludeと簡単なマクロに留めよ。 ネストするマクロ展開禁止。トークンの合成禁止。
- 2レベル以上のポインタの間接参照禁止。typedefでポインタをそうじゃなく見せかけるの 禁止。関数ポインタ禁止。
- 開発初日から常に、コンパイラの警告レベルを最高にしても警告が出ないようなコードを書け。
1, 2, 3あたりはええええって感じだし、8, 9あたり禁止されると 私なんかはプログラムが書けなくなりそうな気がするんだけど、 これも経験に裏打ちされた話なのだから、こういうのが要求される 世界があるってことでしょう。宇宙とか。
ちなみに1, 2, 3, 9あたりは静的検証ツールを使うことを前提にしていて、 静的検証ツールが追いきれないコードは書くなって意図のようだ。
ところで興味があるのは、コンパイルが通ればバグはまず無い、と豪語するような 強い静的型言語ならこういう条件を言語側でサポートできるかってこと。 少なくとも1, 2, 3あたりは静的に処理量の上限が決まって欲しいってことだから MLやHaskellの型システムだけじゃ検証できないよね。依存型ならできるのかな。
昔、comp.lang.lispあたりで静的型vs動的型のflame合戦が起きた時に、 某毒舌Lisperが、「俺は静的型でバグが潰せるというのはまやかしの安心だと 思っているが、静的検証ツールでバグが潰せるというのは信じている。 マルチタスクのタイミング絡みの非常に微妙なバグを、静的検証ツールで 見つけたことがあるからだ。あれは人間が見つけるのは不可能だ」みたいな 発言をしていた気がする。そう、時間が絡む話も普通の静的型言語は まだ扱わないよね。扱えるのかな。
Tag: Programming
2006/10/23
Roombaを試してみている。 「ガベージコレクションならやっぱりLisp (by 竹内郁雄)」だしね。 30日試して気に入らなければ返せるので、まあ期待せずに使ってみるかって感じ だったのだが、思ったよりも綺麗にしてくれる。うちはほとんど全て木のハードフロア ってこともあるだろうけど。ベッドの下とか今まで届かなかった ところも掃除してくれるし。同じところを何度も行き来したりと効率は悪く、その 仕事ぶりを注視していると不安になるんだが、正しい使い方は十分に時間を取って 放っておくことのようだ。僕等の21世紀には万能フランクも勤勉ビーバーもいないが 少なくともRoombaはいる。
ただ、らむ太は機械を見ると目の色を変えて襲いかかり押せるボタンは全て押し 外せるパーツは全て外すまで離さないので、何としてもらむ太に 気づかれないようにしなければならない。これは、外出前にこそっとRoombaを起動 し、帰宅直後に隠すことで何とかなるんじゃないか、と思っているが自信はない。
さて、今日は夕食の買い出し中に仕事部屋を掃除しようと 外出直前にRoombaを放ったのだが、その動作音をリビングから聞きつけた らむ太が突進して来た。あわててドアを閉めてにこやかな笑顔を作り 「さ〜お出かけだ〜」と抱き上げてみたものの、らむ太は疑わしそうに 閉まった仕事部屋のドアを見ている。済まん、らむ太。大人になるということは 秘密を抱えるということなんだ。今に君にもわかる時がくるさ。
この時、勢い良くドアを閉めたのが悪かったのかもしれない。
買い出しから帰ってらむ太の注意をビデオでそらし、仕事部屋の 様子を見に行くとドアが開かない。ちなみにドアは部屋の内側に向かって開く。 Roombaがドアの向こうに居座っているのかと思ったが、Roomba本体はそんなに 重くない。すぐに理由はわかった。ドアの対面に折り畳み式のレジャーチェアが 立てかけてあったのだが、それが倒れてちょうどつっかい棒になってしまっているのだ。
Roombaが衝突して倒れたのだろうか。いやおそらくはドアを閉めた勢いだろう。 ともかく力いっぱいドアを押しても出来る隙間は2cm程で、手を入れることもできない。 仕事部屋の入口はそこ一箇所。窓は空いているが2階であって、足場になるような 庇などはない。12尺ほどの梯子があれば窓から入れるがそういう梯子の持ち合わせもない。 ドア破壊など強制手段を取るにしても、得物となりそうな道具は全て仕事部屋の中だ。 ああRoombaがもっと賢くて人語を解し、ついでにアームか何かがついてて 力仕事もこなしてくれれば…
とりあえず焦っても仕方ないのでいつも通りらむ太に夕食をやり、風呂に入れ、 遊びの相手をしつつ戦略を考えた。と言っても出来ることは限られる。 結局、針金ハンガーをばらした針金で根気良く探ってひっかけるという 原始的な方法で解決した。
しかしこんなことがあると、Roombaをhackして カメラとwifiをつけようか、などと邪な考えが湧いてきてしまうな。
Tag: 生活
2006/10/16
ハワイ大停電
朝7時過ぎ、らむ太に朝食を食べさせている時に地震を感じる。 珍しいものだと思っていたら程無く停電した。
PCはUPSでしばらく生きていたが、ISPの方が落ちたらしくて ネットはつながらず。車のラジオでスキャンすると、ほんの数局しか入らない。 ここでどうやらかなり広域の停電だと見当をつける (実際は、州全域で停電していた)。 この時はどの局も録音番組だったが、8時過ぎからライブでニュースが始まる。
昼過ぎ、車で食糧の買い出しに出た。近場はどこも閉まっている。 Diamond Head Grillの売店が空いていたので適当に購入。 Pearl Cityの方で電気が戻り始めたとの報。
2時過ぎ、らむ太を連れてWaikikiのビーチ方面へ散歩。大きめのホテルや コンドは大抵コジェネを回していたが、エレベーターと非常灯くらいしか 賄えないらしい。部屋にいても仕方ないのか、ホテルのロビーや 歩道は観光客で溢れていた。ABC Storeは内部の冷気を逃さないためだろうか、 扉を締めて入場制限をかけていて、どこも外側に長い列ができていた。
その後、家族で車を出して街の様子を見てみる。ドンキホーテ(旧ダイエー)は やはり長蛇の列。しかしちょっと離れたTimes Supermarketはそうでもない。 マッチの残りが心細かったので(うちはガスなのだが、電気式点火装置は当然 動かない)、ライターを購入したり。 ラジオの報道では島のあちこちで電気が戻り始めているらしい。 夜までに戻るだろうか。 州知事は地震発生時にたまたまハワイ島にいたらしいが、すぐにオアフに 戻ってCivil defense emergency operating centerで指揮を取っているそうな。 このcenter、Diamond Headのクレーター内にあるそうだ。そんなものがあったとは 知らなかった。
らむ太が寝たので一緒に昼寝。PCが動かないから仕事もできない。
日が暮れたがまだ電気は戻らない。キャンプ用のColemanのガスランタンを点火。 外に出るとSt. Louis Heightsなど山の方は 灯りがついているので、こっちももうすぐだろうと希望をつなぐ。 せっかくなので停電のWaikikiを見に行く。
8時すぎ、真っ暗なトイレに入っていたら家の裏手で喚声が上がった。 うちの裏まで電気が来たらしい。しかしうちを含む数軒がまだ。 電気のグリッドって、ひとつのブロック内でも数系統に分かれているらしい。
9時近くなって、らむ太を寝かしつけついでにまた車を出すかと思ったところで 電気が戻った。文明とはありがたい。らむ太を風呂に入れてなんだかんだして ようやくPCを立ち上げた。
Tag: 生活
2006/10/14
YouTubeについてはGoogleの買収意図とか無許諾コンテンツの問題とかの 話題がホットなわけだけれど、それはその方面の人に任せておいて、 一ユーザとしての楽しさを考えると、やはり自分のコンテンツを 気軽にネットに置けるというところだと思う。
今までだって自分のサーバスペースにムービーファイルを置くことは できたわけだけれど、なんというか、わざわざそこまでして見せたいものが あるかと考えるとちょっと壁が高い。それが、あれだけたくさん アップロードされてれば、大したことなくたってちょっと自分も のっけてみようかって思うわけだ。
これは、動画のリリースが気軽に出来るようになったということだ。 未完成でも早めにリリースして反応を見て改善してゆけるような コンテンツにとっては、その利点は大きい。映像作品そのものを そんなふうに反復的に作るのはちょっと難しそうだけれど、 動画でしか伝えられない「何か」を反復的に改善してゆくのに 非常に役に立つんじゃないか。
ということを実際に動画をアップロードしてみて思ったのだった。 先日、かみさんとらむ太が帰省している時に、 ピアノを弾いてるところを撮ったものだ：
どちらもまだまだ未完成だけど、リリースすることで役に立つ フィードバックが貰えている。らむ太がいると全然弾けないので 次はいつになるかわからないが、また撮ってアップロードしてみたい。 数年後になるかもしれないが…
Tag: Piano
2006/10/11
昨年、撮影に参加した短篇映画"Makani Lapule (Sunday Wind)"が、 Hawaii International Film Festivalに通ってたらしい (cf. 20050614-movie-shooting)。 一回だけだが上映される。
http://www.hiff.org/filmlisting_tickets/synopsis.php?id=242
初めての映画撮影だし、他のメインキャストはSAGの人だし、 自分にとってはいろいろ学べた良い経験だったのだが、 正直、監督の求める素材を提供できていたかどうか甚だ心許ない。 でもフィルムは焼き付けられたものが全てであって、言い訳は効かない。 舞台とは別の厳しさがある。 今回出来なかったことは次回のチャンスにできるようになっていなければならない。
Tag: 芝居
Comments (2)