抽象的データタイプの記述言語としての代数的仕様記法

摘要

形式的仕様記述の1つとして抽象データタイプ（Abstract Data Type，以下ADTと略記）の記述言語（ADT Description Language，以下ADTDLと略記）を提案する。ADTはその値の集合Vと、Vの要素に適用可能な演算の集合Fを指定することで定義できる。具体的に集合Vの要素がどのような成分から成っているかを観測する関数の集合と、演算集合Fに含まれる各演算を表す関数（状態遷移関数）の2つの関数の集合を定義し、各観測関数の値が各状態遷移関数の適用によってどのように変化するのかを、公理によって記述する。本研究では実際に作成したテキストエディタの仕様をADTDLで記述することを試みた。テキストエディタを実現するための各種のADTを記述し、階層的にテキストエディタ自身を1つのADTとして記述した。その結果、仕様記述として簡潔で矛盾なく記述でき、ADTDLの実用性が確認できた。