Griesの導出法によるObject-Z仕様からのプログラム導出

スポンサーリンク

概要

• 論文の詳細を見る

• Object-Z(VDM,Z)などの集合に基づいた形式的仕様記述言語は,概念的なモデルで仕様化するシステムの状態空間を表現し,その状態空間に作用するオペレーションを定義するものである.これらは概念的な設計が可能なものである.その反面,これらの仕様記述言語は"looseness"を持つ.たとえば,インプリメントのデータ構造を規定しない,論理和などで記述された仕様の実行順序が非決定的であるなどがある.このような問題により,これらの仕様は,実行不可なものである.本稿では,これらの問題点を解決するための1つのアプローチを提案する.これを検証をするために仕様記述/導出実験を行った.実験例として,"ソフトウェア仕様記述と設計に関する第4回国際ワークショップ"の課題の1つである図書館問題を取り上げる.

• 一般社団法人情報処理学会の論文
• 1992-09-28

著者

• 谷津 弘一

  日本ユニシス株式会社ソフトウェア開発部

• 染谷 誠

  日本ユニシス株式会社ソフトウェア開発部

• 宮崎 比呂志

  情報処理振興事業協会

• 染谷 誠

  日本ユニクス

• 山崎 誠一

  NTTソフトウェア研究所

• 谷津 弘一

  日本ユニクス

• 宮崎 比呂志

  富士通

関連論文

• クリーンルーム手法味見
• Griesの導出法によるObject-Z仕様からのプログラム導出
• システム要求分析技法C-NAP IIと支援ツール : (IV)支援ツール
• 移動体通信システムへの仕様記述技術の適用上の課題
• 統合ソフトウェア開発環境"ソフトウェアCAD" : 事務処理システム開発の場合
• 統合ソフトウェア開発環境"ソフトウェアCAD" : 分析・チェック機能と計算機言語生成機能
• 統合ソフトウェア開発環境"ソフトウェアCAD" : ドキュメント編集機能
• 事務処理システムへのAdaの適用とその評価
• Ada向け構成管理の一考察
• Object-Zのための要求定義と形式的プログラム導出

スポンサーリンク