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

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

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

Number of Access:308（2025-05-07 14:14 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27442

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
IEICE_J78-D_7_622 pdf None 888 KB 216 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

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