はじめに

このディレクトリで提供しているドキュメントは、CafeOBJ の初学者への手引きである。主に自然数の仕様を例題として用い、仕様記述から証明までの流れを体験してもらうことを主眼に置いている。

このドキュメントは、次のように構成されている:

CafeOBJ 処理系の使い方
CafeOBJ 処理系の起動と終了方法
仕様の記述法
仕様を CafeOBJ 処理系に読み込ませる
CafeOBJ の基本的な文法などの仕様の記述法
コメント
モジュール
ソート
輸入
オペレータ
等式
変数
定義済みモジュールの表示
項の構文解析
項の簡約
証明譜を用いた証明法
証明譜とは
組み込み述語 =
結合律の証明
交換律の証明
補足
トラブル発生時
内蔵モジュール
識別子で日本語を使う
練習問題
How to use CafeOBJ processor
Start and Quit
Describing specifications
Reading specifications
Fundamentals of CafeOBJ
Comments
Modules
Sorts
Imports
Operators
Equations
Variables
Show
Parse
Reduce
Verification with proof scores
Proof scores
Equality predicate =
Associativity of +
Commutativity of +
Appendix
Troubleshooting
Built-in modules
Exercises

改訂履歴


Original Copyright © Takahiro Seino, all rights reserved.