Introduction
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

Start and Quit

The reader are assumed to use Unix-like OS and to already install CafeOBJ system in a directory in $PATH.

Start and CafeOBJ prompt

Let '%' be a prompt. Typing 'cafeobj', then CafeOBJ system is started. Hereafter an execution result (and a CafeOBJ source file) is displayed in a rectangle and a word to be typed by the user is underlined.

% 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>

When starting CafeOBJ, the above welcome message is shown, and then CafeOBJ system waits for the user's input with the prompt 'CafeOBJ>'. CafeOBJ prompt will be changed into a word ending with '>', for example, 'NAT>', '%NAT>' and so on.

Quit

To quit CafeOBJ, type 'quit' (or just 'q'):

CafeOBJ> quit
[Leaving CafeOBJ]
%

[Next] Describing specifications