| 研究概要 |
(1)プログラムの性質を表す論理式を動的に生成し,生成された論理式の正しさを証明する研究を継続して推進した.特に,シリンダー分解やグレブナ基底法の応用研究を行った.グレブナ基底の計算の単項順序を工夫することにより,幾何学的な証明問題が効率よく行われるので,多くの実例についてこれを実証するとともに,ウェブプログラムに対しての応用の方策を検討した.また,これらの方法を安全面でクリティカルなコード内に存在するループや,文字列探索のプログラムの検証に適用する研究を継続して行った.
(2)文字列解析によるウェブプログラム検証の研究を継続した.本年度は,スクリプト言語プログラムにおいて重要な役割を果たす正則表現マッチングの研究を重点的に行った.多くのスクリプト言語が採用している欲張り戦略による実装の意味をモナドの概念を用いて定式化し,マッチングに精密に対応する出力付きオートマトンを構成する方法を与えた.この出力付きオートマトンを用いることで,文字列解析の精度を高めることができた.
(3)前年度に引き続き,XML文書と変換規則との効率の良いマッチングアルゴリズムを,より大きなクラスの変換規則に適用することを目指した.今年度はヘッジではなく列に関する正規表現から検討を開始した.まず,前年度に研究を開始していたPOSIX準拠のマッチングのための効率のアルゴリズムをまとめ,発表した.この結果に基づき欲張りマッチング(greedy matching)に基づく効率の良いアルゴリズムを設計することができた.現在は,このアルゴリズムの正当性の検証を続けている.
|
