はじめに
CafeOBJ の使い方: CafeOBJ の起動・終了; 仕様の記述; 仕様の読み込み
CafeOBJ の文法: コメント; モジュール; ソート; 輸入; オペレータ; 等式; 変数; 定義済みモジュールの表示; 項の構文解析; 簡約
証明譜を使った検証: 証明譜とは; 組み込み述語 =; 結合律の証明; 交換律の証明
補足: トラブル発生時の対応; 内蔵モジュール; 識別子で日本語を使う; 練習問題

CafeOBJ の起動・終了

ここでは、主に Unix 系 OS 上で動作する CafeOBJ について説明する。CafeOBJ がパスの通ったディレクトリにインストール済みであることを仮定する。

CafeOBJ の起動と CafeOBJ プロンプト

仮にシェルプロンプトを '%' で表す。CafeOBJ を起動するには、シェルプロンプトから 'cafeobj' とタイプする。コンソールの画面は四角で囲い、タイプライタフォントで表す。タイプすべき文字は下線を付けて表す。

% cafeobj
-- loading standard prelude
;; Loading file /usr/local/cafeobj-1.4/prelude/std.bin ...
;; Loading of file /usr/local/cafeobj-1.4/prelude/std.bin is finished.

          -- CafeOBJ system Version 1.4.6(PigNose0.99,p2) --
                   built: 2003 Nov 17 Mon 4:54:00 GMT
                         prelude file: std.bin
                                  ***
                     2003 Nov 27 Thu 23:17:29 GMT
                            Type ? for help
                                  ***
                  -- Containing PigNose Extensions --
                                  ---
                            built on CLISP
  2.29 (released 2002-07-25) (built on snowrabbit.local [127.0.0.1])
CafeOBJ>

CafeOBJ が起動されると上記のような起動メッセージが出力され、プロンプト 'CafeOBJ>' を出して、入力待ち状態となる。CafeOBJ のプロンプトは CafeOBJ の内部状態によって 'NAT>' や '%NAT>' など、'>' で終了する様々な文字列に変化する。

CafeOBJ の終了

CafeOBJ を終了するには、CafeOBJ プロンプトから、コマンド 'quit' (または、その省略形 'q') をタイプする:

CafeOBJ> quit
[Leaving CafeOBJ]
%

[Next] 仕様の記述