Object-Zのための要求定義と形式的プログラム導出

概要

論文の詳細を見る
通常,プログラムの仕様記述は,構造化プログラムなどの図的な表現によって記述される,あるいは,自然言語で記述されるのが一般的である.図的なプログラム仕様などでは,制御の流れなどに依存したものとなる.したがって,仕様の意味論の抽象化がされておらず可読性の低いものとなる.また,自然言語による仕様では,自然言語による仕様では,自然言語の暖昧性などにより一意的な解釈ができずに,仕様本来の目的を果たさない場合がある.このような問題から,仕様やプログラムの意味論の抽象化が可能であり,暖昧さのない仕様記述方法が必要となる.この問題を解決するのが,論理式などで表す形式的仕様記述法である.一方,形式的仕様記述言語であるObject-Zなどは,実行不可能なものである.したがって,プログラムに結びつけるためには,仕様の内容を解釈して,それ同値と思われるプログラムに変換せざるを得いない.それゆえ,この変換の際に誤ったアルゴリズムを導く可能性もあり,厳密に仕様記述した意味が失われる場合がある.本稿では,Object-Z仕様記述のための分析/設計法と,仕様から正しいプログラムに変換するための方法について,図書館問題を例題として述べる.
一般社団法人情報処理学会の論文
1993-09-27

Object-Zのための要求定義と形式的プログラム導出

スポンサーリンク

概要

著者

関連論文

スポンサーリンク