|
対話的定理証明によるソフトウェアの検証について以下の研究を行った
1) 関数型言語のコンパイラで用いられるCPS(Continuation Passing Style)変換と呼ばれるプログラム変換の形式化と検証を行った。形式化と検証には、束縛変数に関する同値性を直接扱えるNominal Logicに基づく定理証明系Nominal Isabelleを用いた。CPS変換をNominal Isabelleで形式化する場合、変換が導入する新しい束縛変数の扱いが難しく、紙の上の証明をそのまま翻訳することができない。本研究では、必要となる補題を系統的に準備して証明を行うことで、定義や証明の主要な部分を自然な形で記述するができることを示した
2) ウェブプログラム検証の基礎として、スクリプト言語PHPの操作的意味論の研究を行った。PHPは、値を代入するときにコピーを行うCopy-on-Assignmentが基礎となっている。一方、実装には、書き込みの時にコピーを行うCopy-on-Writeが用いられている。本研究では、これら二つの評価戦略に対して、グラフ書き換えによる操作的意味論を与えた。これらの意味論に基づき、PHPの実装が用いているCopy-on-Writeが正しくCopy-on-Assignmentを実装していないことを示した。さらに、この問題の解決した評価戦略としてMostly Copy-on-Assignmentを提案した。また、操作的意味論の核となる部分を定理証明系lsabelle/HOLにより形式化し、基礎的な性質の証明を行った。
|
