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

Comments

CafeOBJ specifications are expected to be read not only by computers but also by human. So, comments are important as well as codes. CafeOBJ supports four kinds of comments as follows:

A line beginning with one of the four keywords '-- ', '** ', '--> ' and '**> ' is a comment.

CafeOBJ system just skips the following comments:

-- This is comment.
** This is comment.

The following comments stand for echo back comments:

--> This is comment.
**> This is comment.

Tips

Although the following is not an official way of comments, it is useful because it can comment out several lines at once.

A block between "" (double quotations) will be skipped. So, you can comment out a block as follows:

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) .
}
"

This unofficial comment cannot be nested.

[Next] Modules