関数型言語ML向け形式的検証支援システムの試作

才村, 徹也; 岡野, 浩三; 谷口, 健一

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2004, 104(243), 13-18

アクセス数:418件（2025-07-06 14:57 集計）

固定URL: https://hdl.handle.net/11094/27448

閲覧可能ファイル 

ファイル フォーマット 利用条件 サイズ 閲覧回数 利用開始日 説明 information
itr104_243_013 pdf なし 698 KB 57 2014.04.11  

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル
関数型言語ML向け形式的検証支援システムの試作
A verification support system for functional programming languages ML
カンスウガタ　ゲンゴ　ML　ムケ　ケイシキテキ　ケンショウ　シエン　システム　ノ　シサク
著者
著者名
才村, 徹也 ; サイムラ, テツヤ ; Saimura, Tetsuya
NRID
1000070252632 1000070252632
著者名
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000000029513 1000000029513
著者名
谷口, 健一 ; タニグチ, ケンイチ ; Taniguchi, Kenichi
キーワード等
関数型言語
ML
形式的検証
プレスブルガー文
functional laguage
formal verification
Presburger sentences
抄録
本稿では,関数型言語ML向けの形式的検証支援システムの試作の概要について述べる.本システムでは,検証者はモジュールのインターフェイス定義ファイルのコメント中に,要求仕様として,前提条件(入力の満たす性質)と後置条件(出力の満たすべき性質)を等式論理で記述し,仕様がプログラムにおいて満たされていることをプレスブルガー文真偽判定アルゴリズムなどを用いて判定する.本システムは,実用的な関数型言語MLプログラムを対象にした検証支援系であること,性質記述を同種の情報と共に記述することでドキュメントとしての情報を充実させること,またその開発言語としてもMLを用いることで,完成したシステムを用いてシステム自体を検証するという利点があることに特徴がある.
This paper presents a formal verification support system for a functional programming languages ML. The system requires a designer to describe pre-conditions and post-conditions as requirements in a comment area of each interface definition file. It decides the conformance between the program and the specification via decision procedure of Presburger sentences. The proposed system has the following features;(1) it aims at one of useful functional programming languages, ML;(2) the proposed description scheme has a natural way to enrich the value of whole document products;(3) it can be an example for our proposed method.
出版者
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
収録物名
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻(号)
104(243)
ページ
13-18
刊行年月
2004-07-27
言語
日本語
ハンドルURL
https://hdl.handle.net/11094/27448
PISSN
09135685
NCID
AN10013287
アクセス権
open access
権利情報
Copyright © 2004 IEICE
本文データはCiNiiから複製したものである
出版タイプ
Version of Record
カテゴリ
学術雑誌論文 Journal Article