Software Verification Based on the Theory of Transducers

点击翻译按钮获取中文摘要

本年度には，以下の研究を行なった．＊ 後方参照を含む拡張正規表現マッチングの計算量解析の研究を継続した．解析の精度を改善するため，集合と木のモナドを組み合わせたモナドを用いるアプローチについて研究を進め，正規表現の微分の考え方を全体に適用することで，これまでより精度の高い解析を実現した．これまでの研究で実装した解析器に本方式を実装し，既存の解析結果と比較した結果，全体の3 分の1 近くの正規表現でオーダの次数が1 以上下がっており, 解析精度が向上されていることを確認できた. 解析の後半は，Berglund らによる非決定性トランスデューサの出力増加率判定に基づいているが，解析内で用いられる複数の変換を組み合わせて単純化するなどの改良を行なった．＊ 先読み付き文脈自由文法は文脈自由文法と解析表現文法（PEG）の両方を拡張したものである．本年度の研究では，まず，先読み付き言語の区間に基づく意味論を導入した．この区間による意味論は，3値論理に基づく意味論に理論的には完全に対応するものであるが，より形式言語理論の古典的な意味論に近いものになっている．また，先読み付き正規表現の微分を先読み付き文脈自由文法の微分に拡張し，微分による所属判定の計算量が文字列長nに対して，O(n^3)となることを示した．＊ トランスデューサを用いたソフトウェア検証の基礎として，自然言語で書かれた仕様を自然言語処理を用いて形式化する研究を行なった．古典的な半単一化を用いた処理と，Transformer を用いた機械翻訳を組み合わせることで，HMTL5字句解析仕様の主要部分を形式化することができた．