抄録
代数仕様言語CafeOBJは,柔軟なmix-fix構文,部分型をともなった強力な型システム,数種類の輸入,パラメータ化モジュール,ビューによるパラメータの具現化などを持つ洗練されたモジュールシステムなどの特徴を持つ.CafeOBJ仕様は代数を意味する.代数は,抽象データ型や抽象機械などの現実のシステムの記述に有効なモデルを包含する汎用性のあるモデル化の枠組みであり,形式仕様の作成と検証を統一的に扱うことができる.本論文では,代数仕様言語CafeOBJの構文および意味について解説する.またCafeOBJ処理系を用いた構文解析,仕様実行,仕様検証についても簡単に解説する.
CafeOBJ algebraic specification language features flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, etc. CafeOBJ specifications denote algebras. The algebra is a universal modeling framework including useful models like abstract data types and abstract machines, and allows us to describe and verify formal specifications in a unified framework. In this paper, the syntax and semantics of CafeOBJ algebraic specification language are explained. The use of CafeOBJ processor also is explained briefly by examples of parsing, executing, and verifying specification.
