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

高阶函数语言的软件模型检查

基本信息

批准号：
12J08057
负责人：
佐藤亮介
金额：
$ 1.28万
依托单位：
The University of Tokyo (2013)Tohoku University (2012)
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2012
资助国家：
日本
起止时间：
2012 至 2013
项目状态：
已结题

项目摘要

高階モデル検査を用いた高階関数型言語のためのソフトウェアモデル検査器の拡張に関する研究を進め、その成果を論文として投稿した。検証の枠組みの拡張として、既存の高階関数型言語のための自動検証手法では扱えなかった関数の等価性や単調性などの関数の性質を扱えるようにした。具体的には、このような関数の性質に関する検証問題を既存の検証手法で扱える問題に帰着する方法を提案した。既存の高階関数型プログラムの自動検証手法のほとんどは、量化子を含まない一階の述語を用いてプログラムを抽象化することによって検証を行っている。しかし、量化子を含まない一階の述語という制限のため、関数の等価性など、全称や関数を用いないと表すことができない性質を扱えなかった。例えば、次のように定義された二つの関数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 0here 所以、sum 是计算 1 到 n 之间的整数之和的函数，sum2 是使用累积变量计算它的函数。在本研究中，我们提出了一种方法，将这种不使用通用名称和函数就无法表达的验证问题减少为仅处理现有一阶谓词的验证问题。基于这个扩展的验证框架，我们为用函数式语言 OCaml 的子集编写的程序实现了原型验证器。我们将所实现的验证器应用到各种程序中并证实了该方法的有效性。目前取得的成果在国内会议上进行了展示，同时与其他研究人员交换了意见。