Akihito Nagataの
ページへようこそ
You are th Comer!

今日はC言語の lex, yacc書き。
面倒だ。 ocaml{lex,yacc}や便利だなと思った。 lexとyaccが通ってもgccが通らないし。 覚えること多過ぎ。疲れました。

ファミ通を立ち読みしたら、 「三国無双」の日本の戦国時代版の「戦国無双」ってのが出るって書いてあった。
真・三国無双２が出たころに、２ちゃんねるのこれのスレッドに、 よく戦国無双が出て欲しいって書いてあるのを目撃しましたが、 ホントに出るみたいだ。 コーエイの人が２ちゃんねるを見たかどうかは知らないけど。
とりあえず出たら買ってしまいそう。

「ケイゾク」

トリックに引き続いて、ケイゾクもレンタルして見てみることにした。
ケイゾクは、 僕の大学１年の時に部活のキャプテンをやってて、 今では早稲田セミナーの講師もやってる大先輩がおもしろいと言ってたので、 大いに期待ができる。

ストーリーは捜査が難航して、お蔵入りしてしまった過去の事件を、 何年にも渡って継続して捜査していく部所に、 東大出身の新米刑事が配属されて、 過去の事件をガシガシと解決していくという話。

とりあえず、１話と２話を見ました。
非常につまらなかった。

何がよくないのか。

• 冒頭の伏線っぽいものは結局なんにも絡んでこない。
• 演技がそれなり。下手じゃないと思うけど、わざとらしさを感じてしまう。
• 話の展開が読める。
• 全部解き明かされた後も、なんとなく疑問に残る点が多い。
• 継続捜査ならではの特徴はない。普通の推理物。

これから先も見るかどうかは微妙。 暇だったら見る。

「日本IBM科学賞授賞式」

	小林先生日本がIBM科学賞授賞だ。 なんだかよくわからないけれどすごいらしい。 過去の日本のノーベル賞授賞者がいっぱい来てたし、 大臣様とか来てた。 ４５歳以下の研究者がとれる賞の中では、 日本で最高だとかなんとか。 小林先生と一緒に論文書けてよかった。 自慢になります。
先生を含めて、６人の方が授賞されていた。 コンピュータサイエンスだけの賞ではなくて、 物理とか化学の研究も対象となるみたい。 賞状の授与のあとに、 授賞者それぞれの研究内容のプレゼンテーションがあったけど、 情報以外の方々の内容はよくわからなかったです。 すごそうだなぁという感じ。 小林先生の発表の比喩はおもしろくてよかった。 やはりわかりやすいプレゼンテーションは 言語系の研究者の悩みのようだ。 聴衆がかなり大物ぞろいだったためか、 小林先生はかなり緊張してた。
	式には先生のご両親や奥様もいらしていた。 先生のお母様とは仲良く慣れそうな空気を感じました。 あれは愛知県民の間合いだ。 式の休憩の間に、どさくさ紛れに一緒に写真を撮ってもらった。 こんな荘厳な式にスーツも着ずに行ってしまった僕です。 米澤研の学生みんなで相談した結果、 スーツじゃなくていいやってことで、 みんなで私服で参戦したところ、 思う存分浮いてしまいました。 誰だ？私服でいいって言った奴は！ なんかもうすでに先生は顔が疲れておりますな。
懇親会。 きっとすごい人がいっぱいいると思われる会。 ちょっとお話してみたかったが、 誰が誰やらわからずなにもできなかった。 仕方ないので、料理の高そうな物を狙っていっぱい食べた。
	その後は内輪だけで田浦さん主催の飲み会だ。かなり気楽だ。 米澤研と小林研と小林先生の昔の仲間の方々が参加。
いやーほんとにおめでとうございます。 小林先生から切っても切れない仲の岩間氏から、花束贈呈。
	なんか、先生は 明後日が誕生日な上に、 来春にお子様が生まれる予定らしいですね。 そりゃめでたいこと尽くしだ。 そんな先生にはキティちゃんも贈呈。 日頃から精神面を支えてくれると言う奥様にもよろしくお伝えください。
楽しかった。久しぶりな人にも会えたし。 また会いましょう。

「User Mode Linuxの作者のJeff Dikeさんの話を聞いた」

わからないことはなかったけど、 やっぱり細かいところは知識が足りなくて理解できなかった。 この人は研究とかそういうのではなく趣味で UMLを作ったらしい。 素晴らしいです。 自分もそうありたいもんだ。

ノートパソコンにVMwareをインストールしました。 今 2000をインストール中。 あんまり早いノートではないんだけど、そこそこの早さで使えたらいいな。 基本的にパワーポイントさえ使えれば満足なんだけど。

最近急に寒くなりましたね。 雪降らないかな。

今日はバイトの研修で今から汐留に行ってきます。では。

研修終った。 内容も微妙だった上に、終電ぎりぎりだったよ。 はーぁ。

研究が進んだ。

リージョンSchemeのC言語への変換器、 および SchemeのためのC言語で書かれたライブラリが完成しつつある。 相変わらずセグメンテーションフォルトとの戦いが大変だった。 C言語でプログラムが書ける人はすごいと思う。 悪戦苦闘して、やっと フィボナッチが動いた。 あとはライブラリを大量に増やせば、 他のプログラムもどうにか動きそうな感じはある。

まだ = と + , - しか動かないので、まだまだ追加の必要あり。 今日は consを追加した時点で力つきました。 また明日。

なんか土日のバイトの疲労をひきずってて、 なかなか立ち上がれなかった。ぐったり。 ミーティングも集中して聞くことができなかった。 いかんなぁ。

そういう状況を打開すべく、夜は研究室の皆様と焼肉を食いにいった。 上野の竹弥。 なんか会話を楽しむより、純粋に食うことを楽しんでしまった。 焼肉うまい。 カニもうまい。 元気になれそう。

そして研究室に戻ってきたらまた寝てしまう。 今、やっと元気になって scheme用のライブラリをCで書いてます。 同じことを何回も書かなくてはならん。 心の底からめんどくさい。

「エクソシスト」

を見ました。 ディレクターズカット版。

うちの父が大好きな映画で、前々から見たかったんだけど、 なんとなく見る機会がなくて、やっと見ることができました。

説明するまでもないですが、かなり昔のホラー映画です。 悪霊に取り付かれた子を２人の神父がお払いします。
ホラー映画って、 "序盤は エロシーンが満載で、後半は血を吹き出しながら人が大量に死んでいく。"というイメージ(１３日の金曜日くらいしか見たことなかったので)でしたが、 エクソシストは意外にも残酷なシーンは少なくて、ストーリー自体が面白かった。 大満足です。 (悪魔払いのシーンにもうちょっと盛り上がりが欲しかった気がするけど)。 漫画の元ネタになっていそうなとこも、いろいろありました。

こういう面白い映画がずっと前からあったのに、今まで見たことなかったのが悔しい。 あまり映画を多くみる人間ではなく、 有名な映画もほとんど見たことないので、 新しい映画を見るよりも、古い名作映画を見た方が楽しいことが多いです。

次は「ジョーズ」と「ウエストサイドストーリー」あたりを狙ってます。

前回に引続きアルバイトやってきました。
イベントのスタッフ。 風船配ったり、来てくれたお客様に案内したり説明したり。

前回はとある駅の近くでテント張ってやっていて、 寒かったり雨が降ったりして、お客様を呼び寄せるのが大変だったけど、 今回は某ビルの一番下の噴水前でイベントやってて、 屋内な上に周りにショッピングモールもあったので自然と人がやってきて、大混雑する中でお客様の案内をするのが大変だった。 お子様は一度転んで泣いてしまうと、風船あげようがお菓子あげようが 泣きやんでくれないし。大変。

ビンゴ大会とかあったんだけど、 人が集まり過ぎて 後ろの方のお客様は番号が聞こえなくてイライラを隠せないご様子。 怖い。
適度に人が集まるところでやるのがよいかと思いました。

インターネットの体験コーナーがあったんだけど、 周りの人が見ている中、一生懸命アダルトサイトを御覧になるお父様や、 いろいろいじって勝手に設定をお変えになる小学校１、２年のお子様が印象的だった。

僕：「パソコンに詳しいんだね。」
お子様：「まぁね。 でもこれXPでしょ？ 僕９８慣れしてるからなぁ。」
さようでございますか。

汐留。

就職先の配属面談なぞを済ませつつ、 今日はバイトの研修があるので、汐留センターシティ？へ。

前にも一度来たことがあるけど、 やっぱりいろいろあるようで何もないとこだなという感じ。 服を見ようかと思ってもMENSは１、２店しかなかったし、雑貨やもソニプラくらいしかないし。 日テレビルもそれほどみるとこないし。 劇団四季の公演を見に来る人と、つじりで甘いもの食べに来た人と、 あとは近くのオフィスで働いてる人で９割を占めてるように見えた。

オフィスが近くにいろいろあることもあってか、 食べ物が充実してた。 特に持ち帰りができるようなものが多かった。
その中からパスタを持ち帰ってセンターシティの中にある公園みたいなところで食べました。
おいしかった。これならOLさんも満足だ。

そんなこんなして時間を潰してたら、 集合時間３０分前に、キャンセルの電話がかかってきた。 なんてこった。 ドタキャン。

「異文化コミュニケーション(NOVAじゃないけど)」

就職関連で英語の勉強をしなくてはならなくなりました。 １２月から４月まで、 週一回くらいのペースでネイティブで英語を話す人と電話で１０分くらい会話をします。
今日はその電話の日でした。
僕はホントに受験英語だけで、海外にも行ったことないので、電話を待ってる間はドキドキだ。

電話の相手はトルコ人のお姉さん。
年は２７歳。
大宮に在住。
休日は池袋でショッピング。
残念ながら既婚者。

１０分間でこういう内容の話をした。
俄然 英会話の勉強をやる気がおきてきた。

Cのプログラムでも書いてみようか。

そろそろC言語へのトランスレータができそうなので、 その中で使用するライブラリを作成する。
あんまりCでプログラムって書いたことないし、書くこと自体が久しぶりなので、 わからないことがいっぱい。
typedefの構文とか、関数ポインタの定義とか、 可変長引数の関数とか人に聞きまくって書いた。 相変わらずなんでもありの言語だと思いました。

昨日が発表だったので、あんまりやる気がでないながらも実装をちょっとずつ進める。
Schemeのletrecは自由過ぎて、きれいにコンパイルできなそうだから、 束縛される値は関数だけに限定することにした。 そしたらさくさくっと進んだ。 最初からこうしておけばよかった。

Camlのメーリングリストで、 design by contractの話がちょっとあがってたように見えたけど、 時間がないから後でって思ってたらどっかにいってしまった。

「発表。」

内容は論文：「Inserting Safe Memory Reuse Commands into ML-like Programs」のサーベイです。

MLみたいな言語は、基本的にリストを作ったりするときに自動的に新しいメモリセル が割り当てられて、GCで回収されるんだけど、 ひとつのセルを何回も使い回せたら、メモリの確保も解放もしなくて実行効率がよくなると思われるので、 静的にプログラムを解析することで、そういった再利用可能なセルを見つけてあげようという論文。

直接の関連研究と言うわけではないですが、 僕もメモリの回収を静的にやる研究をやってるので、 興味を持って調べてみました。

なんかノーテーションとか解析方法が汚くて、強引な感じはあったけど、 結果だけ見れば 少なそうなオーバーヘッドでたくさんのセルを再利用できるような 解析ができていて、 よさげな感じがしました。
僕は今まで静的な解析と言うと、MLの型推論の拡張ようなものしか知らなかったけれど、 これはセマンティクスを Continuation Passing Style(CPS)で定義して、 それに沿った解析をしてるのが新しかった。 こういう解析をやると関数型も手続き型言語みたいにとらえることができるということがわかりました。
Orderdな型システムを使えば、手続き型っぽい解析というか評価順序を踏まえた解析もできるんだけど、 この CPSベースのやり方の方が直観的でいいような気がした。
あと、実装がちゃんとあるのは尊敬しました。 僕もちゃんとしたものを作りたいもんです。

昨日一生懸命やり方を考えてやった発表ですが、 個人的には成功したという感想。 小林先生からも駄目出しはなかったし。 立沢先生からはお褒めの言葉をいただいたし。 成功だ！

今日も今日とて資料作り。
明日発表なのにできてないから。 ぎりぎりにならないとやる気がおこらない人間なので、今日になってしまった。 でも、時間がぎりぎりなのにかなり丁寧に作った。

プレゼンの目標は自分の話を聞いてもらうことで、 自分を見せつける場ではないということを 思っておかねばならんと思う。
自分がわかったこととか、考えたこととか、成功したことの報告もするんだけど、 それがメインになってしまうと、どうもよくないプレゼンになる。
一番に考えることは皆様方に僕の話を聞いていただくということだ。 最初から最後まで、興味を持っていてもらえるようなプレゼンにするのがよいと思う。

自分がプレゼンを聞く立場になって考えると、僕は

• 僕の知らない知識が前提となっていたら、聞きとばす。
• あったかいと眠くなる。
• 細かい話はどうでもいい。
• 話が抽象的過ぎると わかったようなわかんないような気分になる。
• 資料に誤植が一箇所でもあると、資料全体が信用できなくなる。
• 途中でわかんなくなってきたら、そこから先は聞いてるフリをする。
• あんまり細かいこと話されると、そこはわかるんだけど、全体で言いたいことはなんだったかな？と思う。
• 自分の知りたいと思ってる内容がなかなか出てこないと眠くなる。
• 話者がフリーズすると僕の頭もフリーズする。

というようなことを考えながら資料を作りました。

「力尽きた。」

初めて どこぞの海に行ってきました。

	洋風だ。 洋風の海だ。
大砲発射。 発射
	念力で縄が登っていく。 スーパーアラビアン
１００万ドル。 １００万＄で買えてしまうのか。
	光る船が！ 中にはハイテンションのマウス方
ごちそうがおいしかったので 大満足だ。 すべてよし！

寒かったけど、 楽しかった。 乗物よりもイベント重視って感じでした。
子供連れが非常に多く、パパさん達のサービス精神に感涙。 見習わねば。

昨日の日記を頑張って書いたら今日の日記を書く気力がなくなった。
今日は発表の資料を作ったり、 J-Phoneからvodafoneに代わったために 携帯のメアドが変わってあたふたしたりしてました。 研究室のメールボックスが溢れるし。 あたふた。

「Design by Contract! 〜 契約によるデザイン 〜」

はプログラミング言語Eiffelに採り入れられてる概念です。
オブジェクト同士の"契約"を使ってプログラムをデザインすることで、 プログラムの信頼性とクラスの再利用性の向上を狙おうというものです。

class ATM {
  int deposit; 
  pre-condition{x > 0,  deposit > x}
  int withdraw(int x){
    ....
  }
  post-condition{return = x,deposit = old deposit - x}

}

要するに

• pre-condition : 使用側(client)がそのサービスを使用するために、満たすべき条件。
• post-condition : 使用される側(server)が クライアントに対して保証すべき性質(pre-conditionを満たした者に対する義務)

このような、"クライアントとサーバー間のサービスの利用と提供に関する取り決め ＝ 契約" を、 プログラミングの質の向上に利用しよう、 というのが 「Design by Contract(契約によるデザイン)」です。

基本的にpre-condition と post-conditionは実行時に毎回チェックされるので、 デバッグのときは 契約のチェックを ON にして、 製品として出すときは チェックを OFFにして実行効率をあげる、と いうように使用すべきです。
ただ、 オブジェクト指向のプログラム設計のことを考えてみると、 プログラムの開発の単位はクラスであるので、 post-conditionは自分のプログラムで保証すべき性質なのでそれほど重要ではなく、 むしろpre-conditionの方が未知の他人が自分の設計したクラスを使用する上で重要で、これがクラスの再利用性の向上の鍵であることがわかります。
これを踏まえてEiffelはデフォルトでpre-conditionのみチェックするようになっているようです。

残念ながら Eiffel自体はそれほど売れている言語ではないので、 「Design by Contract」も大して役にたたないのかと思ってしまいますが、 Design by ContractはEiffelとは独立して注目を浴びているように見えます。

「Java Modeling Language(JML)」はJavaにDesign by Contractの概念を採り入れた言語です。 Eiffelと同じようにメソッドに対する pre-condition, post-conditionを記述するための特別な構文が用意されています。 ソフトウェア科学会とセキュリティシンポジウム(最近僕が聞きにいった学会)では、 このJMLに関する研究が多数発表されていました。

個人的な意見として、Design by Contactは、 プログラムの質をあげる上で非常に有効な手段のような気がしますが、 使いたいかと言われるとちょっと悩みます。
やっぱりこういう条件を自分で書くのは面倒だし、 厳格な型を持った言語でうまくプログラムを書けばほとんどの条件は書く必要がなるなったりはしないか？と思ってしまいます。 あと、学生ゆえに信頼性が要求されるプログラムを書かなければならない状況に陥ったことがないというのもあります。

学会の発表で論点となっていたのは主に "条件の記述力" と "静的な解析" にあったように思います。
"条件の記述力"は、メソッド1回の実行にかかる時間や、 使用するメモリの量も条件に記述し検証できるようにしよう。というようなものです。
"静的な解析"はEiffelやJMLでは基本的に実行時に条件のチェックがされるのに対し、 このチェックの全てor大部分をコンパイル時にやってしまおうというものです。 pre-condition, post-condition(とあとinvariant)を使って Hoareの公理的意味論を作って、 それの正しさの証明をしようというものです。
静的にチェックが行なえるのであれば、実行時にオーバーヘッドがかからないし、 何よりデバッグが非常にしやすくなるので、 こういう研究はかなり有用な気がします。

僕の結論は「現状では使う気はそれほど起こらないけど、 条件が有効に記述できて、静的に検証できるバージョンの、 Design by Contractな言語ができたら使いたいかもしれない。 」です。
まぁいいや。 Design by Contact バンザイ！

POPLの資料作り。
それっぽくなってきたけど、どの程度詳しく説明したものか迷う。 型判定規則を全部説明するのは避けて、できる限り直観的にわかるようにしたい。 でもそれだけだと、 どうやってるかわかってもらえないだろうから規則もちょっとは載せないと。

ふじもと氏が持ってたMINIXの本をちらっと見てみた。 プロセスの動作の仕方とか書いてあるけど、 ハードウェアの割り込みに対するハンドラとか、 実際にどうやって実装するのか想像つかない。
就職してからOSを作る機会があるとよいな。

全体ミーティング好きだったのに…。 有意義だったのに。 もったいない。 これからはPDSにも出るしかないのか。 あぁ。

また「ギャラクシークエスト」見ちゃった。
これ最高だ。今まで見た映画の中で No1だ！ 今回は英語の勉強のため音声英語で字幕なしで見た。 よくわかんないところもあったので、ネットで発見したスクリプト見つつ、単語調べつつ。
なんだか勉強になったし、笑えたし、感動もしたし(したかな？) かなり満足できた。

全体ミーティングと、POPLミーティングの資料作り。 燃焼系。

部活の先輩が結婚するらしい。
披露宴とかパーティをやらないので、式は自由に参加していいとのことですが、 どうしたものか。
式に出るとなんか邪魔になりそうな気がするけど、 お祝いのプレゼントくらいあげたいと思う。 式に出てもいいんなら出ますけど。 最近部活の人とあんまり連絡とってないのでどうしたらいいかわからん。

スラッシュドットでファミコンの人気ランキングをやってるのを見た。
懐かしい。 上位にいる大体のゲームはやったことあるやつだ。

ここに乗ってないゲームの中で個人的に思いで深いのは「マニアックマンション」というゲーム。たしか同名のホラー映画が題材だった気がする。
謎解きアドベンチャーゲーム。 ７人くらいいた主人公達の中から３人を選んで、マニアックマンションの謎を解く。 選んだキャラによって、壊れたものを直せるなど 微妙に性質が異なり、 後略の仕方が変わる。
アドベンチャーなので、基本的に全部試してみるという方針で始めるんだけど、

• 時間がちゃんと流れてて、時間がたつとマニアックマンションの住人が勝手に動き出して、見つかると捕らえられたりする。
• プールの中を探索してると気に、仲間が誤ってプールに水を張ると、 中にいた奴が水死してしまって、 マンションの前に墓がたつ。 みたいな出来事が多々ある。 ゲームは続行できるけど、クリア不能の気がする。
• 「アイテム」＋「動作」が選択できる。例えば「チェーンソー」＋「切る」とか。 そのせいで、かなりコマンドが多くて全部探索するのが難しい。
• どうでもいい場所でなんかしてもメッセージが出るようになってて、 果してそれが意味があるのかないのかがよくわからない。(少なくとも小学生の僕には)
• ちょっとしたことで屋敷が爆発したりして、全員死んでゲームオーバーなる。

またイベントのバイトやってきました。 某駅の近くで光通信の体験コーナー。 そのスタッフ。

はずかしながら光ネットワークっていうのを初めてさわりました。 ブロードバンドコンテンツとか、 IPテレビ電話とかオンラインゲームの体験しました。

僕はイベント会場の近くで、 通りかかる親子連れのお子様の方に風船をプレゼントしてました。

なかなか楽しい仕事で、 めっちゃ楽しく風船配ってたら、 偶然通りかかったセキミズにその姿を隠し撮りされました。

なんだか思いついたので書いてみる圧縮の話。

"UML" という単語を聞いて、 "User Mode Linux" を思い浮かべる人と、 "Unified Modeling Language" を思い浮かべる人と両方いると思いますが、 ソフトウェア設計の話をしてる場合にUMLと言えば、聞いている人は間違いなく"Unified Modeling Language"の方を指しているとわかると思います。

こういうのを圧縮に使えたら面白いかと思いました。
LZWだったら、 UML を Unified Modeling Language と展開するには、 "UML = Unified Modeling Language" というような情報を辞書で持っておかなければならないけど、 展開する際の状況から判断して UML → Unified Modeling Language と展開できるならば、 そういう辞書を持っておく必要がない。
１００％の確率で戻せるわけではないから、可逆にならないけど、その分圧縮がパワーアップ。

１００個のファイルを圧縮解答するときに、９９個は辞書を作って圧縮解凍して、残りの一個は辞書をつけずに圧縮しておいて、前の９９個用の辞書から統計をとって 最後の一個用の辞書を作るとか。
LZWだと辞書の番号がずれると意味ないから使えないかもしれないけど、 こういうのが利用できる場合ってのはないかな？

あと昨日のwnnの不具合は、個人の辞書を消したら直りました。 /var/lib/wnn/ja/dic/usr/ の下にあった。

上野で三色丼というのを食べました。 あまえびと ホタテとサーモンがたっぷり乗ってます。
めっちゃうまかった。 具だくさんでご飯が足りないくらい。
上野の、刺身とか松茸とかをたたき売りしてるあたりです。
多分材料は築地直送。 一杯 ５５０円 。安い！

ブロードバンドコンテンツってのでおもしろいのないかなー ってずーっと見てたら時間が過ぎていった。 結局おもしろいのなかったよ。

なんか Wnnくんがエラー吐きます。 BAD ERRORNO!!! って。 なんか前にもこれ見たことあるんだけど、直しかたがわかりません。 個人の辞書設定を消せばなおったような気もするけど、 思い違いかもしれないし、そんな設定見当たらないし。 どこも変更してないんだけどな。 誰か教えてください。

「セキュリティシンポジウム。」

の感想文。自分で聞いたやつだけ。ただ内容をメモしてるだけの場合もある。
１日目は午前はうだうだしてたので、午後から行きました。

• MSR 3.0 : The Logical Meeting Point of Multiset Rewriting and Process Algebra
  MSRってのはプロトコルかなんかの使用記述言語 ＋ 証明器(？)。 前バージョン MSR 2.0 では状態遷移の記述しかできなかったけど、 3.0 でプロセス計算の要素も入れてみた。でも完全にプロセス計算を入れてしまうと嫌なことも起こるので、 適度に状態遷移とおり混ぜて導入した。 と言っているような感じがした。よくわかりませんでした。
• A Formal System for Analysis of Cryptographic encription and Their Security properties
  この話はソフトウェア科学会の時も聞いたのですが…、よくわからず。 説明が細か過ぎて大枠がよくわからない。 多分プロトコルの仕様記述と証明のような気がする。
• INference on Honesty in Compositional Logic for Protocol Analysis
  駒場で授業を受けたことのある 慶応の岡田先生の発表。プレゼンの資料よりも岡田先生に目がいってしまう発表だった。 そしてよくわからず。
• A Model for Delimited Infomation Release
  情報流解析の話。 型に機密度の高さを付加して、大事な情報が洩れてないかどうかを静的に検証できる。 機密情報を外に出したい時は 指定された関数を使って機密度を下げてから。
• Detecting Unknown Computer Viruses
  Anti Virusとかはウィルスのデータベースを持ってて、 知ってるウィルスしか検知できないけど、 怪しいプログラムが APIを使う時にフックを書ければ未知のウィルスにも対応できるのではないか？ という話。 できるかもしれないけど、新規ウィルス検出のためのポリシーは与えられなかった。
• UML Scrapbook and Realization of Snapshot Programming Environment
  UMLはUser Mode Linuxの方。 UMLを改造して、UMLの実行状態を保存、複製、復帰できるようにした。 楽しげ。 OSレベルの実行状態を操作できます。開いてたファイルとか同じUML内でのコネクトは維持できるらしい。 さらに、 UMLの状態操作のためのAPIを用意したのでスナップショットを対象としたプログラムが書けるようになるらしい。 用途はモデルチェッキングなど。
  発表者は萩谷研のポッターさん。
  これで一日目終了。
• Reception
  ＠東工大の１００年記念館 というところ。なんか終始 小林先生と前田さんと話してた。 楽しかったし飯もおいしかったからいいけど。 その後は３人で仲良く帰った。
• Java Program Verification at Nijmegen: Developments and Perspective
  ２日目。 Javaのコメントの部分に、 メソッド毎にPre-Condition, Invariant, Post-Conditionを書けるようにした言語 JMLを設計。 それらのメソッドの条件を Hoare論理の式に変換して PVSという定理証明器を使って証明できるようにした。 という話。 どこまでがこの発表の範囲かはよくわからなかった。
  Design by Contractって感じ。
• Verifying Confidentiality and Authentication in Kerberos 5
  朝の電車の中で見かけた人の発表。 普通の人かと思ってたら、どうやらアメリカの海軍の人のようだ。
  内容は ケルベロスのバージョン５が正しいことの証明。
• The Interface Definition Language for Fail-Safe C
  末永がびびってておもしろかった。
• Securing RPC with a reference monitor for system calls
  パケットのフィルタリングを使って、悪意のあるリモート接続をから身を守るのではなく、 リファレンスモニターを使って、RPCの呼出時にフックをかけて、 プロシージャの引き数を見て悪意があるかどうかを判断したら、 柔軟にできるんじゃないかという話。 リファレンスモニターというのはよく知らないけど、 OSとかモジュールをやってる人には一般用語らしい。
• Lunch
  東工大の近くの商店街でおいしい定食を食べた。 ちょっとだけ高級そうなそば屋の昼食。 おいしかった。 ９００円。 当たりでした。
• Formal Specification and Verification of Resource Bound Security Using PVS
  プロシージャに、その中で使用するメモりの量と そのプロシージャの実行時間の上限(Bound)の情報をできるようにする研究。 その上限が守られているかどうかは、条件をHoare論理に変換して、PVSを使って出来る限り静的に証明する。 静的に証明出来ない部分は動的に確かめるので 100％守らせることができる。
  でも、この発表が２０分も時間オーバーしてしまい、チェアの先生に 「発表時間の上限も守れ」と言われてた。
• Cost estimation calculus for analyzing denial-of-service attack resistance
  既存研究で、サーバーとクライアントの負荷を検査し、サーバー側にやたらと負荷が偏ってたら、 サーバーがクラックを受けていると判断する研究がある。 これは負荷の量を適当に計ってたけど、 型を利用して評価時にかかる負荷をより正確に計れるようにし、 負荷の偏りの度合とかがより正確に計れる上に、 負荷の計算がより汎用的になったという話。
  ハーフオープンしてくる攻撃とかDOSは検出できるけど、 クラッカーが複数いると検出が難しいらしい。 あと、プログラムの最適かにも利用できそうですね、というコメントがあった。
• Decision Procedures for Several Properties of Reactive System Specification
  OSとか、 あとエレベーターを制御する装置は、 長時間動作してユーザーと相互にアクションするわけですが、 そういったアプリケーションに対し、時相論理を利用した使用記述言語を定義して、 正しさの検証を可能にした。という話。
• Handcuffing the Big Brother : How to Escrow Transaction Data While Preserving Privacy
  面白そうだったけど、理解できなかった。固有名詞と見られるところの単語が、全然見なれないものばかりだったのだけれど、 あれは英語ではなかったのでしょうか。ドイツ語？
  悪意のある人からデータを守りたい時に、 鍵を持ってる人と持ってない人の２種類に分けてアクセス制限を行なうけれど、 そう単純には分けられない場合があるので、 あるデータベースに書き込む場合には A,B,C,Dの４つの鍵が必要、 とかそういう風にしようって話だったのかな？ 自信ない。
• Formal analysis of e-services through process algebra tools & techniques
  e-サービスのための使用記述言語の設計？ 中身を知らない場合も扱えるから、 openなシステムにも使えるし、 一部分だけ見て検証もできる。 という感じだったと思うのですが。 もう疲れてました。
• Formal Analysis of the NetBill Electonic Commerce Protocol
  OTS, CafeObjってのを使うと、 NetBillの商品のお届けまでプロトコルに加えて検証できるぞって話。 もはや集中力があんまりなかった。

レイアウトがかわったALCは使いにくい。 研究室のサーバーに辞書が大量に入っているはずなので、どうにかそれを利用できないかと模索。
emacsからは引けるんだけどちょっとめんどいので、どうにかコピペ等のマウス操作だけで辞書が引けるようにならないかなと。
サーバーに入ってる辞書はndtpっていうプロトコルで引けるということがわかった。 なんか簡単なプロトコルだったから自分でなんか作れそうだったけど、 tclのGUIクライアントがすぐに見つかったから使ってみた。
それほど使いやすいってわけでもないけど、前のALC並の使いやすさはある。 よかったよかった。

Xファイル見ながら作業しようかなと思ったら、 DVDにプロテクトがかかってる模様でパソコンから見れない。 残念。

遅ればせながら mozilla-1.5 にバージョンアップ。
処理がちょっと早くなった気がする。 あと前から使ってたテーマが使えなくなったのが残念。 しかも他のテーマをダウンロードしようと思ったら、どれも downloads disabled になってるし。まぁいいけど。
あと相変わらず背景画像が固定の場合のスクロールがやたら遅い。 こことかでスクロールするとかなり重い。

「ジュンク堂をぶらぶら。」

なんかおもしろい本はないかなーと。
コンピュータ関連の本はそんなに目新しい本もなくて、 欲しい本はだいたい研究室にあったりするので、なんかトキメかなかった。
諦めて語学のコーナーに。
最近は自分の英語力の無さをひしひしと感じているので、 それを自然に解決できるような楽しく学べる英語教材を探す。

ドラえもんの英訳版があった。他にもいろいろ。 でも英語の吹き出しごとに日本語訳が書いてある。 日本語が書いてあったら先にそっちを読んじゃうじゃないか。 これがなかったら買うのに…。

アメコミでもいいから１００％英語の漫画がないかなと思って、 ９F 洋書コーナーに。
あんまり種類はないけど、 バガボンドの英語版がある。 ちょっとだけ読んでみたところ、おもしろい。 続きが読みたい。 バガボンド読んだことないし。
買おうかなーっと思ったけど、 価格が２７００円だ。
漫画一冊２７００円か。 非常に高いな。 でも２７００円で漫画も読めて英語の勉強にもなると思えば安いのか。 でもやっぱ高い。
そういう風に迷ってたら一日が過ぎた。 優柔不断。 O型。

欲しいけど２７００円は高いな。 うーむ。

今日は東京は霧がかってましたね。 珍しい。

「もう１１月かぁ。」

学生生活もあとわずか。

英語の勉強がしたい。Real playerで英語のニュースをよく聞いてるけど、あ んまりよくわかんない。 語彙力がないのか聞き取れないだけなのか。
でも研究関連の話はなんとなーくわかるから、 一般的な単語の語彙力が足りないのかも。
というわけで英語の新聞も読むことにしました。

今日は発表のための論文読み。 一日型推論。 疲れた。

なんか花の連休なのに日記の内容が冴えないので、一生懸命考えましたが、 やっぱり冴えなかった。 冴えないな。
明日こそ。