Kinoshita Yoshiki

木下 佳樹 教授

所属
情報学部
計算機科学科
関連リンク
専門分野

ソフトウェア科学、プログラム意味論

キーワード

Profile

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

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

プログラムというものは思い通りに動くのが当然、と思いがちですが、実際にはなかなか思い通りに動いてくれません。予想通りに動かない場合は、プログラムに間違いがあるはずです。間違いがないかどうか確かめるのは簡単、試しに動かしてみればいい、と思われるかもしれません。しかし、実はそれはとても難しい。
たとえば会社の事務仕事のプログラムのテストを考えましょう。プログラムに入力するかもしれないデータが何億何兆も無数にあることはすぐわかります。その全ての場合についてテストすることは実際には不可能です。一方、飛行機の制御ソフトウェアを考えてみると、実際に飛行機を飛ばして行うテストは、たとえ一回かぎりでも大変な労力がかかります。それを何億回も繰り返すなんてとてもできません。
テストにはいろいろ問題があるので、別の方法が考えられています。プログラムに何が書いてあるか、文面をよく分析し、「こう書いたプログラムはこう動くことになっている」という事実を積み重ねて、確かにプログラムが思い通りに動くかどうかを推論する方法です。プログラムが思い通りに動くことの「証明」をするわけです。

プログラミングの科学

・プログラムとは何か?(算譜意味論)
・正しいプログラムとは?(算譜検証論)
・システムが妥当とは?(妥当性確認論)

これらが我々の研究室の基本的な問いです。プログラムを書くだけでなく、書いたプログラムが思い通りに動くかどうか検証することを考えます。このようなプログラムを書きたいという「思い」を厳密に書き下ろしたものは「仕様」と呼ばれます。仕様そのものが矛盾していたり、仕様が法律や倫理さらには危機管理などの多角的な要求を十分考慮していないために問題が起こる場合もあります。この場合は、プログラムがいくら仕様通りに動いても、やはり問題が起こってしまいますので、仕様の妥当性確認も必要です。このようなことを追究していくと、一般にプログラムはどんな性質をもっているのかという問題につきあたります。自分が書く、あるいは自分に関係のある特定のプログラムのことではなく、プログラムの一般論を考えることになっていくのです。こういうわけで、我々は、プログラム“で”研究するのではなく、プログラム“を”研究するのだ、といっています。
プログラムをどのようにして書くか(プログラミング)についても、我々は大きな関心をもっています。そもそも、仕様通りに動かないプログラムができないようなプログラムの書き方はないだろうか、という問題意識があります。
さらに、我々が最近研究しはじめたのがシステムの「人的要素」の部分です。ソフトウェアがうまく働くには、その運用や保守などの機械ではなく人間が操作する過程がうまく働く必要があります。このような過程を、プログラムが思い通りに動いていることを証明するテクニックを使って分析できるのではないかと考えています。さらに、企業や役所などの人間による組織も分析できないか、と考えることもあります。まあ、これはちょっとまだ思いつきの話ですけれど。たとえば企業はいろいろな法律や政令などのルール、業界のルール、自社が作ったルールなどに従って仕事をしています。こういうルールは、私たちの世界のプログラムと同じように見ることができそうです。プログラム分析の手法が、会社の経営分析にも適用できるのではないか、そんなことも夢想しています。

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

私は常々、真理そのものに向き合う態度を大切にしたい、と考えています。「偉い人がそう言っているから」あるいは「大勢の人がそう言うから」といったことは、ものごとが正しいかどうかの理由にはなりません。「千万人といえども我行かん」という気持ちを忘れず、他の人が何を言っているかとは別に、自分自身でものごとを確かめる態度を大切にしたい。
一方、ものごとを他人に伝えることは、真理を知ったり確かめたりすることとは別です。自分が知って確かめたことを、何でもかんでも他人に伝えるべきとは限らないようです。これは他人に話すべきことなのか、また、話すべきなのであれば、どのように話せばわかってもらえるか、ということに意を用いることも大切だと、最近気づき始めているところです。
これらは、自分でそうしたいと思いながら、なかなかできずにいることです。学生諸君と一緒に、このような態度を身に付けた人間になっていけるように努めていきたいと思っています。

プログラミング科学研究室

プログラミングの原理を科学する

当研究室のテーマである「プログラミング科学」とは、プログラムとは何か?(算譜意味論)、正しいプログラムとは?(算譜検証論)、システムが妥当とは?(妥当性確認論) という三つの問いから出発する、プログラム構築に関する科学です。 算譜意味論には圏論、普遍代数などを用います。算譜検証論には、命題論理や述語論理だけでなく、時相論理や構成的型理論などの特別な体系を用います。妥当性確認論では、アシュランスケースと呼ばれる形式を用います。 当研究室では、算譜意味論や算譜検証論の手法を応用した形式アシュランスケース、システム利用者を含めた情報処理システムライフサイクルなどを数理科学の立場から研究しています。

Photos

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

  • これはコーヒー豆を挽くグラインダです。平塚では大島を眺めてスローライフを送り、来し方行く末を考えようという魂胆で、電動ではなく手動のを使っています。横浜に移っても大島の代わりに横浜港をながめて過ごしましょう。学生時代に生協で手に入れた同じ型のものが、今でも自宅にあります。鋳物で適当な重さがあるところが気に入っていますが、長期のデフレにも関わらず値段は三倍にあがりました。鋳物職人が減って価値が上がったのかななどと想像しています

SDGsの取組み

地域課題

SDGs・地域課題について

Recommend

他の先生もチェック!