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

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

このアイテムのアクセス数:41件（2021-06-20 09:26 集計）

このアイテムへのリンクには次のURLをご利用ください:http://hdl.handle.net/11094/27448

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
itr104_243_013	pdf	698 KB	20

論文情報

タイトル	関数型言語ML向け形式的検証支援システムの試作
別タイトル	A verification support system for functional programming languages ML
タイトル (ヨミ)	カンスウガタ　ゲンゴ　ML　ムケ　ケイシキテキ　ケンショウ　シエン　システム　ノ　シサク
著者	才村, 徹也才村, 徹也
	岡野, 浩三岡野, 浩三
	谷口, 健一谷口, 健一
著者の別表記	Saimura, Tetsuya
	Okano, Kozo
	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
ISSN	09135685
NCID	AN10013287
URL	http://hdl.handle.net/11094/27448
権利情報	Copyright © 2004 IEICE
権利情報	本文データはCiNiiから複製したものである
言語	日本語
カテゴリ	学術雑誌論文 Journal Article

著者版フラグ	publisher
NII資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
dcmi資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス.104(243) P.13-P.18
DC.title	関数型言語ML向け形式的検証支援システムの試作
DCTERMS.alternative	A verification support system for functional programming languages ML
DC.creator	才村, 徹也
	岡野, 浩三
	谷口, 健一
DC.creator	Saimura, Tetsuya
	Okano, Kozo
	Taniguchi, Kenichi
DC.publisher	電子情報通信学会
DC.language" scheme="DCTERMS.RFC1766	日本語
DCTERMS.issued" scheme="DCTERMS.W3CDTF	2004-07-27
DC.identifier" scheme="DCTERMS.URI	http://hdl.handle.net/11094/27448
DC.subject	関数型言語
	ML
	形式的検証
	プレスブルガー文
	functional laguage
	formal verification
	Presburger sentences
DCTERMS.abstract	本稿では,関数型言語ML向けの形式的検証支援システムの試作の概要について述べる.本システムでは,検証者はモジュールのインターフェイス定義ファイルのコメント中に,要求仕様として,前提条件(入力の満たす性質)と後置条件(出力の満たすべき性質)を等式論理で記述し,仕様がプログラムにおいて満たされていることをプレスブルガー文真偽判定アルゴリズムなどを用いて判定する.本システムは,実用的な関数型言語MLプログラムを対象にした検証支援系であること,性質記述を同種の情報と共に記述することでドキュメントとしての情報を充実させること,またその開発言語としてもMLを用いることで,完成したシステムを用いてシステム自体を検証するという利点があることに特徴がある.
DCTERMS.abstract	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.
DC.rights	Copyright © 2004 IEICE
DC.rights	本文データはCiNiiから複製したものである
citation_title	関数型言語ML向け形式的検証支援システムの試作
citation_author	才村, 徹也
	岡野, 浩三
	谷口, 健一
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	2004-07-27
citation_journal_title	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
citation_volume	104
citation_issue	243
citation_firstpage	13
citation_lastpage	18
citation_issn	09135685
citation_public_url	http://hdl.handle.net/11094/27448
citation_keywords	関数型言語
	ML
	形式的検証
	プレスブルガー文
	functional laguage
	formal verification
	Presburger sentences

閲覧可能ファイル

論文情報

論文詳細を表示