研究内容

プログラムの意味ってなんだろう

「虫のいないプログラムはない」といわれるほど、誤りのないプログラムを作るのは大変な作業であることはよく知られている。プログラムの正しさの定式化には、まず最初にプログラムが持つ意味を数学的に定める必要がある。現在、プログラムが持つ基本的な性質の研究を進めており、効率的な計算のための計算戦略やプログラムの持つ性質を自動証明するための枠組みやその基礎技術、与えられたプログラムと意味が同じであるがより効率的なプログラムに変換する方法などについて研究している。これらを通して、信頼性が高くて効率の良いソフトウエアの作成法の開発を目指している。

●プログラムの数学的モデル項書換え系
項書換え系は、0+x→xのように式の変換を定義する規則の集合である。入力として与えられた式を規則により変換して最終的に得られた式を出力と考えることにより、これをプログラムモデルと考えることが出来る。 項書換え系は、このような単純なモデルではあるが計算能力は他の言語と変わらないことが分かっている。そこで、項書換え系の研究の他に、それを関数型言語に応用するために超えるべきギャップである、関数をデータとして扱う機能である高階性や適用する規則の優先順序をもつ場合への拡張を行っている。

• 計算の停止性の研究

一般に書きやすくて誤りの少ないプログラムと、効率良く実行できるプログラムは異なる。前者から後者を生成するプログラム変換を研究している。この他に、逆計算を行うプログラムの自動生成や、生成したいプログラムの性質の記述からその性質を満たすプログラムを自動生成する仕組みについて研究を進めている。

●仕様の検証・定理自動証明
実行不可能な仕様（要求仕様）をプログラム化するためには、これに実現の情報を加えて実行可能な仕様に変換する必要がある。この変換操作は実現と呼ばれるが、一般には自動的に変換できない。このため、何らかの人間の介入があることから検証の必要性が生ずる。代数的仕様の場合には、実現の結果得られた仕様において要求仕様の各々の等式が成り立つことを示すことによって検証される。そこで、この検証の定式化並びに検証支援法について研究を行っている。また、この仕組みを応用して、セキュリティプロトコルの安全性の検証も試みている。 

●SATソルバを利用したお絵描きロジック問題作成ツール