权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

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

基本信息

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

This study aims at the development of support systems for speech detection in relation to digital transformation. Last year, the main elements of the system were discussed (including the size determination of integers). The key to determining the authenticity of a text is the use of digital programming language ML to create and evaluate its usefulness. This year's test method is confirmed, and the test support system is tested. A method for managing the equations along the set of equations and tables for describing the "contract base design" is described. In the second place, the identification formula of this kind of document is automatically created, and the identification method of this kind of document is examined. The identification method was developed in June 2004 in Okayama. In September 2010, the Research Council for Digital Speech ML (OCaML) was held in Hakodate, Japan. The test example is to select the test item and the test item is to create the test item. This is the first time I've ever seen a girl. This is mainly due to the fact that the lower level of the data operation is the same as the upper level of the data operation. The lower level of the data operation is the same as the upper level of the data operation. The result of the test is that the students are not accustomed to the test, and the method is inferior to the time. The results were announced in March 2005(the first year of the 2005 Olympics).