はじめに
このディレクトリで提供しているドキュメントは、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
改訂履歴
- 2008-02-06 「識別子に日本語を使う」を追加した。
- 2007-09-25 「証明譜とは」の証明ログのダンプに誤りがあったので修正した。
- 2007-09-25 「オペレータ」の属性の説明を修正した。
- 2007-09-13 proof score の訳「検証譜」を「証明譜」に変更した。文中の検証を証明に変更した。
- 2006-07-11 組み込み述語 _==_ に代えて、_=_ を使用するように変更した。
[Next] CafeOBJ の起動・終了
Original Copyright © Takahiro Seino, all rights reserved.