Daikonの限定利用によるJavaメソッドの事後条件の自動導出

梶田, 泰伸; 岡野, 浩三; 楠本, 真二

このアイテムのアクセス数:45件（2020-12-05 12:34 集計）

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

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
itr105_332_007	pdf	622 KB	21

論文情報

タイトル	Daikonの限定利用によるJavaメソッドの事後条件の自動導出
別タイトル	Automatic generation of post-conditions for Java methods by limited utilization of Daikon
タイトル (ヨミ)	Daikon　ノ　ゲンテイ　リヨウ　ニ　ヨル　Java　メソッド　ノ　ジゴ　ジョウケン　ノ　ジドウ　ドウシュツ
著者	梶田, 泰伸梶田, 泰伸
	岡野, 浩三岡野, 浩三
	楠本, 真二楠本, 真二
著者の別表記	Kajita,Yasunobu
	Okano, Kozo
	Kusumoto, Shinji
著者 (ヨミ)	カジタ, ヤスノブ
	オカノ, コウゾウ
	クスモト, シンジ
キーワード等	Design by Contract（DbC）
	Java
	事前条件
	事後条件
	Daikon
	JML
	pre-condition
	post-condition
抄録	近年Javaに対するDesign by Contract(DbC)の導入に関心が集まっている.事前・事後条件, 不変表明をアサーションの形でJavaプログラムに記述することで, 契約の取り決めを行うことができる.事前・事後条件, 不変表明を表すアサーションを自動で生成するツールにDaikonがある.しかしDaikonはJavaプログラムの実行時の変数の値の情報をもとに, あらかじめ用意した性質のみをチェックしてアサーションを生成するため, 変数間の関係が複雑である場合はあてはまる性質が存在せず単純なアサーションしか生成できない.そこで本稿ではこれらのアサーションの中でも事後条件に注目し, Daikonをループ部のみに限定して適用しその他の部分は変数をトレースして値を推論することにより, 変数間の関係がより詳細な事後条件を生成する手法について述べる.この手法により, Daikonを単独で利用するより詳細な事後条件を生成することができた.
抄録	Recently, the application of Design by Contract(DbC) to Java is concerned. The contracts can be made by describing pre-conditions, post-conditions, and invariants into the Java programs as assertions. Daikon is a tool which automatically generates assertions such as pre-conditions, post-conditions, and invariants. However, in generating assertions, Daikon checks only pre-defined properties based on the values of variables while running the Java programs. Thus when the relations between variables are complex, Daikon can generate only quite simple assertions because there are no pre-defined properties matching such those relations. In this paper, focusing on post-conditions, we propose a method which enables to generate detailed post-conditions with complex relations between variables. The method applies Daikon to only loop parts of the Java programs, while in the rest parts it traces the values of the whole variables. From a simple experiment. we found that the method generated more detailed post-conditions than Daikon alone.
公開者	電子情報通信学会
公開者の別表記	The Institute of Electronics, Information and Communication Engineers
公開者 (ヨミ)	デンシ　ジョウホウ　ツウシン　ガッカイ
掲載誌名	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻	105
号	332
開始ページ	7
終了ページ	12
刊行年月	2005-10-07
ISSN	09135685
NCID	AN10013287
URL	http://hdl.handle.net/11094/27424
権利情報	Copyright © 2005 IEICE
権利情報	本文データはCiNiiから複製したものである
言語	日本語
カテゴリ	学術雑誌論文 Journal Article

著者版フラグ	publisher
NII資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
dcmi資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス.105(332) P.7-P.12
DC.title	Daikonの限定利用によるJavaメソッドの事後条件の自動導出
DCTERMS.alternative	Automatic generation of post-conditions for Java methods by limited utilization of Daikon
DC.creator	梶田, 泰伸
	岡野, 浩三
	楠本, 真二
DC.creator	Kajita,Yasunobu
	Okano, Kozo
	Kusumoto, Shinji
DC.publisher	電子情報通信学会
DC.language" scheme="DCTERMS.RFC1766	日本語
DCTERMS.issued" scheme="DCTERMS.W3CDTF	2005-10-07
DC.identifier" scheme="DCTERMS.URI	http://hdl.handle.net/11094/27424
DC.subject	Design by Contract（DbC）
	Java
	事前条件
	事後条件
	Daikon
	JML
	pre-condition
	post-condition
DCTERMS.abstract	近年Javaに対するDesign by Contract(DbC)の導入に関心が集まっている.事前・事後条件, 不変表明をアサーションの形でJavaプログラムに記述することで, 契約の取り決めを行うことができる.事前・事後条件, 不変表明を表すアサーションを自動で生成するツールにDaikonがある.しかしDaikonはJavaプログラムの実行時の変数の値の情報をもとに, あらかじめ用意した性質のみをチェックしてアサーションを生成するため, 変数間の関係が複雑である場合はあてはまる性質が存在せず単純なアサーションしか生成できない.そこで本稿ではこれらのアサーションの中でも事後条件に注目し, Daikonをループ部のみに限定して適用しその他の部分は変数をトレースして値を推論することにより, 変数間の関係がより詳細な事後条件を生成する手法について述べる.この手法により, Daikonを単独で利用するより詳細な事後条件を生成することができた.
DCTERMS.abstract	Recently, the application of Design by Contract(DbC) to Java is concerned. The contracts can be made by describing pre-conditions, post-conditions, and invariants into the Java programs as assertions. Daikon is a tool which automatically generates assertions such as pre-conditions, post-conditions, and invariants. However, in generating assertions, Daikon checks only pre-defined properties based on the values of variables while running the Java programs. Thus when the relations between variables are complex, Daikon can generate only quite simple assertions because there are no pre-defined properties matching such those relations. In this paper, focusing on post-conditions, we propose a method which enables to generate detailed post-conditions with complex relations between variables. The method applies Daikon to only loop parts of the Java programs, while in the rest parts it traces the values of the whole variables. From a simple experiment. we found that the method generated more detailed post-conditions than Daikon alone.
DC.rights	Copyright © 2005 IEICE
DC.rights	本文データはCiNiiから複製したものである
citation_title	Daikonの限定利用によるJavaメソッドの事後条件の自動導出
citation_author	梶田, 泰伸
	岡野, 浩三
	楠本, 真二
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	2005-10-07
citation_journal_title	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
citation_volume	105
citation_issue	332
citation_firstpage	7
citation_lastpage	12
citation_issn	09135685
citation_public_url	http://hdl.handle.net/11094/27424
citation_keywords	Design by Contract（DbC）
	Java
	事前条件
	事後条件
	Daikon
	JML
	pre-condition
	post-condition

閲覧可能ファイル

論文情報

論文詳細を表示