関数型プログラムに対するモジュール構造を考慮にいれた効率のよい形式的検証支援

有效的形式验证支持，考虑到功能程序的模块化结构

基本信息

批准号：
14780214
负责人：
岡野浩三
金额：
$ 2.43万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2002
资助国家：
日本
起止时间：
2002 至 2004
项目状态：
已结题

项目摘要

本研究は関数型プログラミング言語向けの検証支援システムの開発を目標にしている.昨年度までにそのシステムの主要ルーチンである(整数上の変数込みの大小判定を含む)プレスブルガー文真偽判定ルーチンを関数型プログラミング言語MLを用いて作成し,その有用性の評価を行なった.今年度は検証手法を確定し,検証支援システムを試作した.まず,モジュールごとに記述された「契約に基づく設計」に沿ったモジュール仕様を等式集合として表し,それらのモジュール仕様の各等式を管理しやすいようにXMLタグを用いて管理する方法を考案した.次いで,この仕様とプログラム本体から検証式を自動作成し,正しさの検証をプレスブルガー文真偽判定に帰着させる判定手法を考案し,その検証手法を6月に岡山で行われたソフトウェアシンポジウム2004(査読あり)にて発表した.次いで,この検証手法に基づき,関数型言語ML向けにOCaMLを用いて作成した検証支援システムを9月に函館で行われたソフトウェアサイエンス研究会にて発表した.検証例題として図書管理システムを選び,プログラム作成と仕様作成を行った.このシステムは大きく6つのモジュールで構成される.この中で主要なモジュールである貸し出しモジュールに対し,下位のデータベース操作モジュールの仕様の正しさを仮定した上で,正しく貸し出しが行われること(そのようにプログラムが実装されていること)の検証作業をこの検証支援システムを実際に用いて行った.その結果,検証作業に不慣れな学生であっても,従来手法と遜色のない手間と時間でできることがわかった.この結果は,3月に行われたPPL2005(プログラムおよびプログラム言語ワークショップ2005)で発表し,デモ公開した.

这项研究旨在为功能编程语言开发验证支持系统。直到去年，使用功能编程语言ML创建了系统的主要例程（包括整数变量的大和小判断），并评估了其实用性。今年，我们确认了验证方法并创建了验证支持系统。首先，我们设计了一种方法，其中模块规格按照为每个模块编写的“基于合同的设计”表示为平等的方程组，并使用XML标签，以使管理这些模块规范的每个方程式更容易。接下来，我们设计了一种方法，在该方法中，通过此规范和程序本身自动创建验证公式，并设计了一种判断方法，该方法可导致对PressBurger句子真实的正确性验证，并在6月在Okeama举行的Software Commposium 2004（同行评审）上介绍了验证方法。接下来，基于这种验证方法，在9月在Hakodate举行的软件科学研究小组中介绍了使用OCAML为功能语言ML创建的验证支持系统。选择了书本管理系统作为测试示例，并创建了程序并创建了规格。该系统由六个模块组成。其中，使用此验证支持系统验证了主要模块，即贷款模块，用于验证贷款模块是否正确借贷（即以这种方式实现该程序）。结果，发现即使是不熟悉验证工作的学生，也可以像传统方法一样努力和时间。结果在3月举行的PPL2005（节目和编程语言研讨会）上介绍，并发布了演示。