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

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

電子情報通信学会論文誌D, 1995, J78-DI(7), 622-633

アクセス数:699件（2025-07-05 19:33 集計）

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

閲覧可能ファイル 

ファイル フォーマット 利用条件 サイズ 閲覧回数 利用開始日 説明 information
IEICE_J78-D_7_622 pdf なし 888 KB 218 2014.04.11  

論文情報

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

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