研究内容

高品質ソフトウェアの構築技術

「高品質のソフトウェア」の条件としては、正しく動作すること、速いこと、メモリ使用量が少ないことはもちろんだが、構造が整っていていること、再利用に適していること、仕様などのドキュメントがしっかり揃っていることなど、ソフトウェア工学的な条件もあげられる。「正しく動作する」の意味はもう少し具体的に言うと、開発者の意図通りに働くこと、および、暴走やフリーズしないなどプログラムの基本的性質をもつことである。これらの高品質プログラムの条件のうち、正しく動作するという条件に注目し、プログラムが正しく動作をすることを検証する方法、正しいプログラムしかできないようなプログラム構成法などを研究課題として研究を行っている。

プログラムが仕様を満たすか？という問題の研究

開発者の意図を書き表したものを仕様という。仕様は、自然言語で表現したもの、論理式として表したもの、分かり易いプログラムで表したものなど、いろいろな形式で記述される。論理式として記述される仕様の場合、それをプログラムが満たすかどうかという問題は、定理証明やモデル検査の問題として捉えられる。この研究では、仕様を等式で表し、プログラムを項書換え系という関数型プログラムのモデルとした場合の問題が帰納的定理の証明問題に帰着されることに着目し、帰納的定理自動証明法について研究を進めている。

仕様を満たすプログラムの自動生成に関する研究

プログラムの開発は段階的に行われる、つまり、既に開発済みのプログラムを拡張して新たなプログラムを開発することが多い。このような開発を自動化することがこの研究の目的である。具体的な研究課題は、既存プログラムとして項書換え系、新プログラムの仕様として限量子付き等式を採用して、それらから仕様を満たす新プログラムを自動生成する手法の開発である。現在検討している手法は、変換規則により仕様とプログラムの対を変換して、最終的に仕様を満たすプログラムを得るというものである。つまり、変換により



を得て、最後のS_nがプログラムになっていればS_nがS₀を満たすプログラムになるような変換規則を考案している。例えば、次のような仕様S₀と既存プログラムP₀を考える。
 
 

P₀は自然数の２分の１を求める関数dのプログラム、S₀は自然数の２倍を求める関数dの仕様である。このような仕様とプログラムの対(S₀,P₀)に変換ルールを適用するとS_nとして



が得られる。

プログラムが基本的性質を持つか？という問題の研究

プログラムが仕様を満たすかという問題とは別に、プログラムの基本的な性質を調べることも重要な課題である。そのような基本的な性質としては、以下のようなものがある。
1.必ず停止すること（停止性）
2.計算結果が一意になっていること（結果の一意性）
3.意図した以外には停止しないこと（デッドロックフリー性）
4.第３者にデータが洩れないこと（機密性）
5.データが改竄されないこと（保全性）
これらの性質毎に異なる検査手法が必要である。例えば、項書換え系の停止性の検査法に関する研究では、効率的にチェックできるような停止性の十分条件の研究を行っている。一方、機密性や保全性というようなプログラムの安全性のチェックには、主に、型の概念を用いる手法を研究している。