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

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

基本信息

批准号：
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)で発表し,デモ公開した.

本研究的目标是开发一个函数式编程语言的验证支持系统。到去年，我们已经开发出了该系统的主例程——Presburger语句真/假判断例程（包括整数变量的大小判断）。使用函数式编程语言ML创建，并对其实用性进行了评估。本财年，我们最终确定了验证方法，并创建了原型验证支持系统。我们设计了一种方法，将根据“设计”的模块规格表示为一组方程，并使用 XML 标签来管理这些模块规格的每个方程，以使其更易于管理。接下来，我们根据该规范创建了一个验证公式我们设计了一种自动创建“Pressburger Sentence”并减少对Pressburger句子真假判断的正确性验证的方法，并在2004年软件研讨会上提出了该验证方法（同行-审查）六月在冈山举行，基于这种验证方法，我们在9月于函馆举行的软件科学研究小组上展示了使用OCaML为函数式语言ML创建的验证支持系统。我们选择图书馆管理系统作为验证示例并创建了一个程序。共六个主要模块，其中以租赁模块为主，制定了下层数据库操作模块的规范。基于正确性的假设，我们实际上使用了这个验证支持系统来验证贷款是否正确执行（程序是这样实现的）。结果，即使是那些不熟悉验证工作的人也发现，即使是学生可以用与传统方法相同的精力和时间来完成。结果在3月份举行的PPL2005（程序和编程语言研讨会2005）上公布并演示。