実行可能な形式仕様言語CafeOBJ(4) : CafeOBJによるZ仕様のアニメーションの枠組み

概要

論文の詳細を見る
仕様を記述する上で、仕様の実行が可能であることは大きなメリットをもたらす。それは、実行により仕様の内容をより深く理解できるからである。Zは集合論に基くmodel-basedな形式仕様言語であり高い表現力を持つが、Zで記述された仕様をそのまま実行することはできない。Z仕様の実行には他言語によるZ仕様のアニメーションが必要となる。本稿では、IPAで開発されている実行可能な形式仕様言語CafeOBJによるZ仕様のアニメーションの枠組みについて述べる。CafeOBJは、代数仕様言語OBJに一方向の書き換え規則を加えたもので、OBJと同様に項書き換え系により実行可能であるという特長を持つ。CafeOBJを用いることにより、Z仕様と同じレベルの抽象度を保ちながらのアニメーションが可能となる。端的にいうと、CafeOBJモジュールは2-categoryを表す。本稿では、まずZ仕様に2-categorica1な解釈を与え、その解釈を基にZ仕様をCafeOBJモジュールで表現するための指針を導くことにより、CafeOBJによるZ仕様のアニメーションの枠組みを明らかにする。
一般社団法人情報処理学会の論文
1994-09-20