2010 Fiscal Year Annual Research Report
形式的に検証可能なプログラム変換フレームワークの構築
| Project/Area Number |
20500011
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
西村 進 京都大学, 理学研究科, 准教授 (10283681)
|
|---|
| Keywords | プログラム理論 / プログラム変換 / 形式的証明 |
|---|
| Research Abstract |
構造化文書XMLにおいて、文書中におけるデータをXMLの構造に関する相対的な位置関係で指定するための標準的な言語であるXPathに関して、その等価性を形式的に推論するためのフレームワークを与え、いくつかの自明でない等価性を導出できることを示した。(本大学院生の池田雄太氏との共同研究)
XPathの相対的な位置関係による当該データの検索は、XMLが表す木構造上での計算を行うプログラムの表現であると考えられ、この等価性を論じることはプログラム変換の正しさを論じることに他ならない。本共同研究では、XPathの式をその入力と出力の間の2項関係として表現し、異なるふたつのXPath式の等価性を関係間の相互の包含関係を示すことによって示した。(ここで関係の包含関係はプログラムの詳細化と対応する。)また、XPathでよく用いられる、条件によるデータの絞り込みを、統一的な方法で2項関係によって表現することができることも示した。これによって、XPathの等価性および詳細化を、関係に関する少数の代数規則を運用することにより、既存の手法より簡潔に証明することが可能となった。実際に証明した等価性にはすでに知られていたものだけでなく、否定命題によるデータの絞り込みを伴うものなども含まれる。また、これまで正しいと信じられていたある等価性が実は等価ではないということをこのフレームワーク上で発見し、これを修正することにも成功した。
この結果を、1月にアメリカ合衆国テキサス州オースティンで開催されたプログラム変換に関する国際研究集会ACM SIGPLAN 2011 Workshop on Partial Evaluation and Program Manipulation (PEPM'11)において発表した。
|
