|
ソフトウェア開発時には、そのソフトウェアに対してどのような性質・機能が要求されているかを厳密に定義する必要がある。一意で明確な定義を与えるために、形式的仕様は重要な役割を果たす。これまで多くの形式的仕様の記述言語が提案されてきた。我々は、記述能力の高さや数学的概念との親和性などから、集合論に基づく形式的仕様記述言語に注目している。このような言語に、ZF(Zermelo-Fraenkel)集合論に基礎を置く仕様記述言語Zがある。しかし、Zでは、集合に対応づけられる仕様中で用いられる部分関数は、一意である必要が置換公理によって求められる。仕様中の情報だけでは、一意であることを証明できない関数を用いて書かれた仕様は、不完全な仕様となる。その部分関数を、一意であることが証明できるように完全に仕様中で定義した時に、設計・実現に関する情報も仕様に書くことになるのであれば、その部分関数を仕様中で完全には定義せずにおくべきである。ただし、その場合、置換公理を満たすために、その部分関数が一意であることを、記述言語が暗黙の裡に保証する必要がある。
そこで、我々は不完全な定義の部分関数を仕様に導入できる言語Z++を定義した。一方、言語Zや、その拡張である言語Z++で書かれた仕様は、仕様を解釈するためのモデルが規定されていないため、一般には直接実行できない。そこで、プロトタイピイングによる利点を享受するために、設計・実現に関する情報を与える記述として実行時仕様を呼ぶ記述を導入した。ソフトウェアの定義を仕様と実行時仕様に分離することで、高いレベルの表現能力での仕様の記述と、実行時仕様に基づく仕様のプロトタイピングの両方が可能になった。本研究では、仕様の解釈としての実行時仕様の与え方とそれに基づく実行の枠組みを対象とした。また、いくつかの問題に本システムを適用した結果に基づいて、その評価を行なった。
|
