高階関数型言語のためのソフトウェアモデル検査

高階モデル検査を用いた高階関数型言語のためのソフトウェアモデル検査器の拡張に関する研究を進め、その成果を論文として投稿した。検証の枠組みの拡張として、既存の高階関数型言語のための自動検証手法では扱えなかった関数の等価性や単調性などの関数の性質を扱えるようにした。具体的には、このような関数の性質に関する検証問題を既存の検証手法で扱える問題に帰着する方法を提案した。既存の高階関数型プログラムの自動検証手法のほとんどは、量化子を含まない一階の述語を用いてプログラムを抽象化することによって検証を行っている。しかし、量化子を含まない一階の述語という制限のため、関数の等価性など、全称や関数を用いないと表すことができない性質を扱えなかった。例えば、次のように定義された二つの関数sum、sum2が等しいということが検証できない。let rec sum n = if n <0 then 0 else n + sum (n-l)let rec sumacc n m = if n <0 then m el se sumacc (n-1) (n+m)let sum2 n = sumacc n 0ここで、sumは1からnまでの整数の和を求める関数であり、sum2はそれを累積変数を用いて求めるものである。本研究では、このような全称および関数を用いないと表せない性質の検証問題を、既存の一階の述語のみを扱う検証問題に帰着する方法を提案した。この拡張した検証の枠祖みを基に、関数型言語OCamlのサブセットで書かれたプログラムを対象とする検証器のプロトタイプを実装した。実装した検証器をさまざまなプログラムに適用し、本手法の有効性を確かめた。ここまでに得られた成果を国内会議の場で発表し、同時に他の研究者との意見交換を行った。

高階モデル検査を用いた高階関数型言語のためのソフトウェアモデル検査器の拡張に関する研究を進め、その成果を論文として投稿した。検証の枠組みの拡張として、既存の高階関数型言語のための自動検証手法では扱えなかった関数の等価性や単調性などの関数の性質を扱えるようにした。具体的には、このような関数の性質に関する検証問題を既存の検証手法で扱える問題に帰着する方法を提案した。既存の高階関数型プログラムの自動検証手法のほとんどは、量化子を含まない一階の述語を用いてプログラムを抽象化することによって検証を行っている。しかし、量化子を含まない一階の述語という制限のため、関数の等価性など、全称や関数を用いないと表すことができない性質を扱えなかった。例えば、次のように定義された二つの関数sum、sum2が等しいということが検証できない。let rec sum n = if n <0 then 0 else n + sum (n-l)let rec sumacc n m = if n <0 then m el se sumacc (n-1) (n+m)let sum2 n = sumacc n 0ここで、sumは1からnまでの整数の和を求める関数であり、sum2はそれを累積変数を用いて求めるものである。本研究では、このような全称および関数を用いないと表せない性質の検証問題を、既存の一階の述語のみを扱う検証問題に帰着する方法を提案した。この拡張した検証の枠祖みを基に、関数型言語OCamlのサブセットで書かれたプログラムを対象とする検証器のプロトタイプを実装した。実装した検証器をさまざまなプログラムに適用し、本手法の有効性を確かめた。ここまでに得られた成果を国内会議の場で発表し、同時に他の研究者との意見交換を行った。