論理型仕様の理解支援のための一手法

概要

論文の詳細を見る
ソフトェア開発においては、ソフトウェアを厳密に定義することが必要である。そのための形式的仕様記述言語として論理型言語がある。論理型言語は、正当性の証明に適しているなどの優れた性質を持つ。しかしその反面、理解性・読解性に必ずしも優れているとは言えない。理解のしにくさの原因として、仕様中のある記述がソフトウェアにおける何を表現しているのかを理解することの難しさが挙げられる。求められるソフトウェアを仕様として定義する場合、定型的なデータ構造やその操作を陰に用いることが多いと考えられる。ここでの定型とは、テーブルやレコードなどのデータ構造やそれに対する操作である。これらの定型は、特定のアプリケーションによらず、普遍的に現れる。このようなよく使われる定型を"概念"と呼ぶことにする。概念はデータ構造とそれに対する操作から定義されるものとする。概念が仕様記述言語によって記述されている場合、読解者はどのような概念が存在するかを記述から推測する必要がある。これは多大の労力を要する。そこで、一階述語論理に基づいた仕様に現れる概念を、定理証明技法を用いることにより仕様の記述から推測し、読解者に提示する手法を提案する.
一般社団法人情報処理学会の論文
1994-03-07

論理型仕様の理解支援のための一手法

スポンサーリンク

概要

著者

関連論文

スポンサーリンク