限量子付き等式仕様からのプログラム生成に関する研究

本研究の目的は,変換規則によりr_i ; r_iをR_<i+1> ; R_<i+1>に変換することを繰り返えしてプログラムを自動生成する方法を開発することである.ここに,E_iは∀とヨを許した等式だけからなる論理式の集合であり,仕様という.R_iは項書換え系であり,実行可能であるのでプログラムとみなせる.R_0は既に開発済みのプログラムであり,E_0はR_0を基礎に新たに定義したい関数の定義である.あるnでE_nが空集合になれば変換プロセスは終了し,R_nが生成されたプログラムとなる.今年度は以下の研究を行った。1.新しい変換規則の考案:新たな関数の仕様を追加する変換規則"Introduction"を導入し,この導入によっても健全性が損なわれないことを証明した.また,この規則が必要なプログラム生成例を示した.2.対話的変換ツールの作成:変換を対話的に進めるためのツールを開発した.変換対象の論理式が複雑になるにつれて変換候補の数が爆発的に増加する問題に対応するために,変換に有効でない候補を除去する戦略が求められる.本ツールには変換候補の枝刈りを行う戦略を組み込んだ.3.その他:本研究が提案する変換に基づくプログラム自動生成法に密接に関係する項書換え系の停止性について,新たな決定可能なクラス解明,既存の証明法の拡張などを行った.

本研究の目的は,変換規則によりr_i ; r_iをR_<i+1> ; R_<i+1>に変換することを繰り返えしてプログラムを自動生成する方法を開発することである.ここに,E_iは∀とヨを許した等式だけからなる論理式の集合であり,仕様という.R_iは項書換え系であり,実行可能であるのでプログラムとみなせる.R_0は既に開発済みのプログラムであり,E_0はR_0を基礎に新たに定義したい関数の定義である.あるnでE_nが空集合になれば変換プロセスは終了し,R_nが生成されたプログラムとなる.今年度は以下の研究を行った。1.新しい変換規則の考案:新たな関数の仕様を追加する変換規則"Introduction"を導入し,この導入によっても健全性が損なわれないことを証明した.また,この規則が必要なプログラム生成例を示した.2.対話的変換ツールの作成:変換を対話的に進めるためのツールを開発した.変換対象の論理式が複雑になるにつれて変換候補の数が爆発的に増加する問題に対応するために,変換に有効でない候補を除去する戦略が求められる.本ツールには変換候補の枝刈りを行う戦略を組み込んだ.3.その他:本研究が提案する変換に基づくプログラム自動生成法に密接に関係する項書換え系の停止性について,新たな決定可能なクラス解明,既存の証明法の拡張などを行った.