2011 Fiscal Year Annual Research Report
形式的に検証可能なプログラム変換フレームワークの構築
| Project/Area Number |
20500011
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
西村 進 京都大学, 大学院・理学研究科, 准教授 (10283681)
|
|---|
| Keywords | プログラム理論 / プログラム変換 / 形式的検証 / 並行プログラム |
|---|
| Research Abstract |
並行計算プログラムに関する安全なプログラム変換に向けての研究を行った。並行プログラムは、近年その重要性が増しているが、並行計算に本質的に内在する複雑さのため、並行計算プログラムを正しく変換するのは容易ではない。困難の原因は並行計算プログラムの適切な形式的モデルの欠如にあると考え、プログラミング言語の意味モデルを具体的かつ正確に与えることができるとして近年研究が進んできているゲーム意味論に基づく形式化を試みた。
この目的のため、プログラミング言語Algolに基づいた並行言語を設計し、そのゲーム意味論を与えた。ゲーム意味論では、プログラムの実行システムとプログラムの2者で交互に手を打つ一種のゲーム上の対局として定式化し、プログラムの実行を2者の打ち手の履歴で表現する。並行プログラムをゲーム意味論で定式化する際問題となるのは、素直に複数のプログラムの実行を混ぜ合わせる(interleave)と上述の2者が交互に手を打つという
条件が崩れてしまうことにある。この問題を、プログラムが一時的に他の並行実行されているプログラムに実行権を譲り、実行権が回復され次第再開する、という動作を表す打ち手を導入することにより解決した。このような定式化が並行実行に関する完全抽象モデルを与えること、すなわち2つの並行プログラムの等価性が、それぞれのプログラムに関する可能な打ち手の履歴(戦略)の等価性に帰着できることを示した。(渡辺敬介氏との共同研究)
また、ある一定の条件を満たすプログラムについては対応する戦略が正規言語で表され、これによって並行プログラムの等価性が判定できることを示した。このことは、並行プログラムの等価性の判定が原理的に自動化可能であることを示唆しており、並行プログラムの安全なプログラム変換の正当性の形式的検証に向けての重要な方向づけになると考えられる。
|
