代数仕様言語は,仕様が実行可能であるという特徴を利用して,仕様をプロトタイプと見倣せたり,検証の半自動化を実現できる.しかし,代数仕様言語が実用に供するには,モジュールを効率よく扱え書換え速度が高速な処理系が必要である.本研究では,実行効率のよい代数仕様言語CafeOBJの処理系を作成し,その処理系が正しく動くことを示すために,以下のことを行った.CafeOBJのモジュールシステムの要求と設計をCafeOBJを用いて記述し,設計が要求を満たしていることを振舞等価の概念を用いて示した.そしてこの仕様記述および検証で得られた仕様記述の際に得られた知見をまとめた.