研究紹介

English version

主要な研究テーマ: 高信頼・安全なソフトウェア構成のための基礎理論とその実践

ソフトウェア基礎論分野では,数学的な厳密さを以てその正しさが保証された プログラムを作成することを究極の目標とし,計算機ソフトウェアに関する数 学的な基礎理論(プログラム理論)を構築する研究を行っている. 最近の主要テーマは以下の通りである.

これらの研究に共通するのは,「論理」をキーワー ドとしているという点であり,論理学に基づいた厳密な手法をソフトウェ アの世界に適用するという考え方である.

最近の研究論文リスト

各テーマの概要

プログラムの検証技術の研究

プログラムを「動けば良い」という観点だけから見る人にとって,基礎理論は 必要ないかも知れない.実際,簡単なプログラムであれば,特に頭を使わなく ても手を動かすだけで自然に書けてしまうことも多い.しかし,書いたプログ ラムがきちんと意図通りに動くことが必要な場合,それでは済まない. 現在の ソフトウェア開発では,プログラムを運用する前にテストを行うことでプログ ラムが正しく動くかを検査しているが,テストだけではカバーできる範囲に限 界があるため不十分である.銀行のオンラインシステムなど社会的に重要度の 高いプログラム,デバイスドライバなどの事前にテストができない(行いにく い)プログラムでは,正しく動くことを,プログラムの運用前に予め厳密 に保証する手法が求められている.そのような要請に答えるためには,ただ プログラムを書けば良いのではなく,プログラムがどのように動いてほしいか, という要求仕様を明確にし,さらに,プログラムがその仕様を満たすことの保 証を付ける必要がある.書かれたプログラムが仕様を満たしているかを確かめる ことをプログラム検証という.

プログラム検証のための基本的な技術には型理論モデル検 査プログラム論理などいくつか代表的なものがあり,それぞれ長 所・短所がある.これまでは,型理論という手法(コンパイラが行う型検査の基 礎理論でもあり,予め決められたエラーを検出するのに向いている)に重きを置 いてきたが,最近はその他の技術との融合も目指している.

この分野では例えば以下のような研究テーマに取り組んでいる.

低水準プログラムにおける資源解放ミスを検出する型理論

C言語など低水準プログラムを困難にしている原因のひとつである,メモリ領 域・スレッド・ロックなどの計算資源の二重解放・解放し忘れによるエラー を発見するための型理論の研究.

高性能計算プログラムの検証

いわゆる高性能計算のためのプログラム はスパコンの性能を最大限に引き出すためにプログラムをチューニングする ため,本来の数値計算アルゴリズムがきちんと表現されているかを確認する のは簡単な作業ではない.本研究ではチューニングされたプログラムと元々 のアルゴリズムが一致することを検証する技術を研究する.

高階モデル検査

モデル検査は,有限オートマトンで書かれたプログラムのモデルが論理式の 形で与えられた仕様を満たすかどうかを全数探索によって検査する手法であ る.プログラム(のモデル)が有限オートマトンで書かれているため,特に高 階関数などを扱うプログラムの検証にそのまま適用するのは困難であった. 本研究は,有限オートマトンではなく,状態数が無限にあるような計算すら 表現できる Higher-Order Recursion Scheme と呼ばれる,より強力な計算モ デルに対するモデル検査を通じて関数型プログラムやオブジェクト指向プロ グラムの検証を行うことを目指している.

ハイブリッドシステムの検証

ハイブリッドシステムとは,制御にソフトウェアが関わっている飛行機等, 力学・電気系の連続量で記述される動作と,ソフトウェアの離散量で記述さ れる動作によって全体の動作が実現されるシステムである.本研究で は無限小プログラミングというアイデアに基づいてハイブリッドシス テムを検証することを目指している.無限小プログラミングとは,ハイブリッ ドシステムを「無限小」を表す定数を含むプログラムとして記述することで, 連続的変化を離散的変化として表現するという手法で,この手法により,従 来手法ではハイブリッドシステムに適用することが難しかったプログラム論 理や型理論等の手法を,ほぼそのままの形で応用することが可能となる.本 研究ではナイーブに無限小を扱うのではなく,Robinson らによって提案され た超準解析と呼ばれる手法によって厳密な数学的議論に基づいてプロ グラムの意味論の定義や検証手法の健全性の証明等を行なっている.

プログラミング言語のための新しい抽象化機構の研究

プログラムを,人から計算機へアルゴリズムを伝えるという手段としてだけで はなく,人から人へと計算システムに関する考えを伝える・共有するた めのメディアであると考えると,それを記述するためのプログラミング言語 も,計算機にとってわかりやすい機械語ではなく,人間にとっても意味がわか りやすいものでなくてはならない.抽象化機構とは,(計算機の)細部を隠すた めのプログラミング言語に備わった機能であり,例えば「手続き」は最も基本 的な抽象化機構である.

我々は,人間にとってよりわかりやすいプログラムが書ければ,自然とプログ ラムの誤りも少なくなるだろう,という考えに基き,アプリケーション 分野に応じた適切な抽象化機構の開発とその理論研究を行っている.

計算と論理の研究

カリー・ハワード同型対応としても知られている「プログラム=証明」とい うテーゼに関して古くから広く研究されていたのは,非常に簡単な構造しか 持たないプログラミング言語と直観主義論理の間の関係であった.我々は, 特に古典論理や様相論理と計算との関連性を考察し,これらの論理が もつ計算体系としての側面を明らかにすることに取り組んでいる.これは必 ずしも単なる理論的な興味に留まるものではなく,例えば,継続例外処理といった制御オペレータをもつプログラミング言語の型理論 と古典論理の証明体系との関連性が指摘されていたりするなど,実際のプロ グラミング言語への応用の面でも重要な研究である.

静的・動的検査の融合(漸進的型付け)の研究

プログラミング言語のほとんどは,コンパイル時に型検査を行いエラーを検出 する静的型付け言語と,エラーの検出は実行時に行う動的型付け言語に分類さ れる.前者は,エラー検出が早い段階でできる安全性というメリットがある反 面,プログラム記述の柔軟性を損なう場合がある.後者はその逆で,柔軟でプ ロトタイピングなどに向いているが,デバグが大変になりがちである.

このテーマでは,動的型付けされるプログラムから,静的型付けされるプログ ラムへの漸進的な移行を可能にするために,動的型付けされる部分と静的型付 けされる部分がひとつのプログラム内に共存できるような枠組み---漸進的型付 けの理論---を研究している.特に,実用的な言語である Java 言語を題材とし て,理論研究を行うとともに処理系の実装を行っている.

多段階計算・プログラミング言語の研究

多段階プログラミングとは,プログラムをデータとして扱うことで,プログ ラムを生成するようなプログラムを組むことを指している.多段階プログラ ミングをサポートする言語機構としてはCやLispのマクロ機能,C++のテンプ レートなどがあるが,いずれも生成されたプログラムが本当に安全な プログラムかを事前に検査することが難しい.我々は多段階プログラミン グをより安全に行うための適切な言語の設計を,様相論理に基づく型 理論を使って行うとともに,そういった言語の実装理論を研究している. これまでの研究成果として,多段階プログラミング言語を実行するための仮 想機械のアーキテクチャを,インタプリタプログラムからの系統的変換によっ て導出することに成功している.

ソフトウェアモジュラリティの研究

オブジェクト指向言語は,継承・部分型といった抽象化機構により高いプロ グラム再利用性(モジュラリティ)を持つ言語として現在のソフトウェア開発 現場でも広く使われている.しかし,ここ15年くらいでオブジェクト指向の 限界が指摘される中で,アスペクト指向・コンテクスト指向といった,オブ ジェクト指向の欠点を補うモジュラリティのための新しい抽象化技術が開発 されてきている.しかし,こういった技術はアイデア先行で理論的基盤が脆 弱であることもありまだ広く使われているとはいい難い.

本研究では,こういった新しいモジュラリティのための抽象化の意味論や型 理論を研究している.

証明支援系

証明支援系(proof assistant)とは,計算機上で数学の証明を書くためのソフ トウェアシステムであり,Coq,Isabelle/HOL などが知られている.証明支 援系を使うことで,証明の正しさを機械的に厳密に確かめることができるが, まだまだその技術は未熟で大規模な理論の検証には専門家の知識が必要であ る.

本研究では,Coq によるオブジェクト指向言語の形式化などを通じて証明の 再利用性などを考察するとともに,証明支援系の改良を考えている.