代数仕様言語CafeOBJは，柔軟なmix-fix構文，部分型をともなった強力な型システム，数種類の輸入，パラメータ化モジュール，ビューによるパラメータの具現化などを持つ洗練されたモジュールシステムなどの特徴を持つ．CafeOBJ仕様は代数を意味する．代数は，抽象データ型や抽象機械などの現実のシステムの記述に有効なモデルを包含する汎用性のあるモデル化の枠組みであり，形式仕様の作成と検証を統一的に扱うことができる．本論文では，代数仕様言語CafeOBJの構文および意味について解説する．またCafeOBJ処理系を用いた構文解析，仕様実行，仕様検証についても簡単に解説する．