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

Describing specifications

A CafeOBJ specification is described in a text file with the extension .mod.

The following is a CafeOBJ specification of natural numbers:

mod! SIMPLE-NAT {
  [ Nat ]
  op 0 : -> Nat
  op s : Nat -> Nat
}

mod! NAT+ {
  pr(SIMPLE-NAT)
  op _+_ : Nat Nat -> Nat
  eq 0 + M:Nat = M .
  eq s (N:Nat) + M:Nat = s (N + M) .
}

Save the above text file as simple-nat.mod in a directory. Be careful about blanks between words (op, s, ., etc) and differences between lowercase and uppercase characters. CafeOBJ system discriminates them.

[Next] Reading specifications