理学部 情報科学科
木下 佳樹 教授
Kinoshita Yoshiki

研究分野 システム検証、プログラム意味論

理学部 情報科学科 木下 佳樹 教授

プログラム“で”研究するのではなく、
プログラム“を”研究する。

このプログラムは思い通りに動くか?

プログラムというものは思い通りに動くのが当然、と思いがちですが、実際にはなかなか思い通りに動いてくれません。予想通りに動かない場合は、プログラムに間違いがあるはずです。間違いがないかどうか確かめるのは簡単、試しに動かしてみればいい、と思われるかもしれません。しかし、実はそれはとても難しい。

たとえば会社の事務仕事のプログラムのテストを考えましょう。プログラムに入力するかもしれないデータが何億何兆も無数にあることはすぐわかります。その全ての場合についてテストすることは実際には不可能です。一方、飛行機の制御ソフトウェアを考えてみると、実際に飛行機を飛ばして行うテストは、たとえ一回かぎりでも大変な労力がかかります。それを何億回も繰り返すなんてとてもできません。

テストにはいろいろ問題があるので、別の方法が考えられています。プログラムに何が書いてあるか、文面をよく分析し、「こう書いたプログラムはこう動くことになっている」という事実を積み重ねて、確かにプログラムが思い通りに動くかどうかを推論する方法です。プログラムが思い通りに動くことの「証明」をするわけです。

「ソフトウェア基礎」と「ソフトウェアデザイン論」の講義では、プログラムが思い通りに動くことの証明を練習します。見方を変えると、プログラムの間違い探しを機械的に行う方法を講義する、ということもできます。プログラムには、実行がそのうち終わることが期待される電卓のようなものと、実行が終わってしまっては困る自動車制御やオペレーティングシステムのようなものとの二つに分かれます。ソフトウェア基礎では前者について、ソフトウェアデザイン論では後者について、プログラムについての証明を講義します。

プログラミングの科学

・プログラムとは何か?(算譜意味論)

・正しいプログラムとは?(算譜検証論)

・システムが妥当とは?(妥当性確認論)

これらが我々の研究室の基本的な問いです。プログラムを書くだけでなく、書いたプログラムが思い通りに動くかどうか検証することを考えます。このようなプログラムを書きたいという「思い」を厳密に書き下ろしたものは「仕様」と呼ばれます。仕様そのものが矛盾していたり、仕様が法律や倫理さらには危機管理などの多角的な要求を十分考慮していないために問題が起こる場合もあります。この場合は、プログラムがいくら仕様通りに動いても、やはり問題が起こってしまいますので、仕様の妥当性確認も必要です。このようなことを追究していくと、一般にプログラムはどんな性質をもっているのかという問題につきあたります。自分が書く、あるいは自分に関係のある特定のプログラムのことではなく、プログラムの一般論を考えることになっていくのです。こういうわけで、我々は、プログラム“で”研究するのではなく、プログラム“を”研究するのだ、といっています。

プログラムをどのようにして書くか(プログラミング)についても、我々は大きな関心をもっています。そもそも、仕様通りに動かないプログラムができないようなプログラムの書き方はないだろうか、という問題意識があります。

さらに、我々が最近研究しはじめたのがシステムの「人的要素」の部分です。ソフトウェアがうまく働くには、その運用や保守などの機械ではなく人間が操作する過程がうまく働く必要があります。このような過程を、プログラムが思い通りに動いていることを証明するテクニックを使って分析できるのではないかと考えています。さらに、企業や役所などの人間による組織も分析できないか、と考えることもあります。まあ、これはちょっとまだ思いつきの話ですけれど。たとえば企業はいろいろな法律や政令などのルール、業界のルール、自社が作ったルールなどに従って仕事をしています。こういうルールは、私たちの世界のプログラムと同じように見ることができそうです。プログラム分析の手法が、会社の経営分析にも適用できるのではないか、そんなことも夢想しています。

誰かがそう言うからではなく、自分自身で真理そのものに向き合う

私は常々、真理そのものに向き合う態度を大切にしたい、と考えています。「偉い人がそう言っているから」あるいは「大勢の人がそう言うから」といったことは、ものごとが正しいかどうかの理由にはなりません。「千万人といえども我行かん」という気持ちを忘れず、他の人が何を言っているかとは別に、自分自身でものごとを確かめる態度を大切にしたい。

一方、ものごとを他人に伝えることは、真理を知ったり確かめたりすることとは別です。自分が知って確かめたことを、何でもかんでも他人に伝えるべきとは限らないようです。これは他人に話すべきことなのか、また、話すべきなのであれば、どのように話せばわかってもらえるか、ということに意を用いることも大切だと、最近気づき始めているところです。

これらは、自分でそうしたいと思いながら、なかなかできずにいることです。学生諸君と一緒に、このような態度を身に付けた人間になっていけるように努めていきたいと思っています。

研究室にある大きな白板
研究室にある大きな白板。ケンブリッジ大学のニュートン・インスティテュート(数学の研究所)を訪ねたとき、所内のいたるところに黒板が貼付けられ、手洗いの中にあるものまでちゃんと使われていることにびっくり。写真撮影の後、この白板も含めて4枚をちゃんと研究室の壁に取り付けて御満悦

愛用のマグカップ
愛用のマグカップ。コーヒーの色がよく見えるので気に入っている