あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法

岡野, 浩三; 東野, 輝夫; 谷口, 健一

このアイテムのアクセス数:145件（2022-05-24 20:22 集計）

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

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
IEICE_J78-D_7_622	pdf	888 KB	147

論文情報

タイトル	あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法
別タイトル	Proof Method for Correctness of Refinements of Algebraic Specification in Abstract Sequential Machine Style
タイトル (ヨミ)	アル　スタイル　ニ　モトヅク　ジュンジョ　キカイガタ　キジュツ　ニ　オケル　ショウサイカ　ノ　タダシサ　ノ　ショウメイ　ホウホウ
著者	岡野, 浩三岡野, 浩三
	東野, 輝夫東野, 輝夫
	谷口, 健一谷口, 健一
著者の別表記	Okano, Kozo
	Higashino, Teruo
	Taniguchi, Kenichi
著者 (ヨミ)	オカノ, コウゾウ
	ヒガシノ, テルオ
	タニグチ, ケンイチ
キーワード等	代数的仕様
	階層的設計法
	射影
	順序機械型プログラム
	プログラム検証法
抄録	代数的手法を用いた階層的設計法として，我々は要求仕様から実現プログラムまで同一の詳細化法に基づいて段階的に順次詳細化する方法を提案している．各レベルでは，そのレベルでの関数，処理の性質等の要求記述が行われ，そのレベルで閉じた記述になっている．上記の方法で順序機械型記述を行う際に，（イ）興味ある関数に対する要求のみ取り出す拡張射影を用いる方法，および，（ロ）通常のように前提条件を内部データに関する具体的な述語を用いて記述せず，外部入力の条件と実行制御上の条件で定義される到達正当性条件を用いて記述する方法等が有用であることが既にわかっている．本論文では，拡張射影あるいは，到達正当性条件を用いて記述された順序機械型記述間において，正しい詳細化であることを形式的に定義し，そうであることを示すための証明方法について新たに述べる．詳細化の自由度を大きな範囲で許しているにもかかわらず，これらの証明方法は従来の記述法に対する証明方法で必要とする手間や，考案すべき言明の量と比べ遜色がない．
公開者	電子情報通信学会
公開者の別表記	The Institute of Electronics, Information and Communication Engineers
公開者 (ヨミ)	デンシ　ジョウホウ　ツウシン　ガッカイ
掲載誌名	電子情報通信学会論文誌D
巻	J78-DI
号	7
開始ページ	622
終了ページ	633
刊行年月	1995-07-25
ISSN	09151915
NCID	AA11341020
URL	http://hdl.handle.net/11094/27442
関連情報 (references)	http://search.ieice.org/
権利情報	Copyright © 1995 IEICE
言語	日本語
カテゴリ	学術雑誌論文 Journal Article

著者版フラグ	publisher
NII資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
dcmi資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会論文誌D.J78-DI(7) P.622-P.633
DC.title	あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法
DCTERMS.alternative	Proof Method for Correctness of Refinements of Algebraic Specification in Abstract Sequential Machine Style
DC.creator	岡野, 浩三
	東野, 輝夫
	谷口, 健一
DC.creator	Okano, Kozo
	Higashino, Teruo
	Taniguchi, Kenichi
DC.publisher	電子情報通信学会
DC.language" scheme="DCTERMS.RFC1766	日本語
DCTERMS.issued" scheme="DCTERMS.W3CDTF	1995-07-25
DC.identifier" scheme="DCTERMS.URI	http://hdl.handle.net/11094/27442
DC.subject	代数的仕様
	階層的設計法
	射影
	順序機械型プログラム
	プログラム検証法
DCTERMS.abstract	代数的手法を用いた階層的設計法として，我々は要求仕様から実現プログラムまで同一の詳細化法に基づいて段階的に順次詳細化する方法を提案している．各レベルでは，そのレベルでの関数，処理の性質等の要求記述が行われ，そのレベルで閉じた記述になっている．上記の方法で順序機械型記述を行う際に，（イ）興味ある関数に対する要求のみ取り出す拡張射影を用いる方法，および，（ロ）通常のように前提条件を内部データに関する具体的な述語を用いて記述せず，外部入力の条件と実行制御上の条件で定義される到達正当性条件を用いて記述する方法等が有用であることが既にわかっている．本論文では，拡張射影あるいは，到達正当性条件を用いて記述された順序機械型記述間において，正しい詳細化であることを形式的に定義し，そうであることを示すための証明方法について新たに述べる．詳細化の自由度を大きな範囲で許しているにもかかわらず，これらの証明方法は従来の記述法に対する証明方法で必要とする手間や，考案すべき言明の量と比べ遜色がない．
DC.rights	Copyright © 1995 IEICE
citation_title	あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法
citation_author	岡野, 浩三
	東野, 輝夫
	谷口, 健一
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	1995-07-25
citation_journal_title	電子情報通信学会論文誌D
citation_volume	J78-DI
citation_issue	7
citation_firstpage	622
citation_lastpage	633
citation_issn	09151915
citation_public_url	http://hdl.handle.net/11094/27442
citation_keywords	代数的仕様
	階層的設計法
	射影
	順序機械型プログラム
	プログラム検証法

閲覧可能ファイル

論文情報

論文詳細を表示