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

Built-in modules

CafeOBJ supports many useful built-in modules. For example, in the built-in module NAT for natural numbers, Arabic numerals like 16384 can be used instead of s(s(...(s(0))...))(*).

(*) NAT is useful for describing and verifying a system which uses natural numbers as a data type, however, it is not suitable for describing and verifying some property of the natural number itself.

Following built-in modules are included in CafeOBJ:

BOOL : Boolean algebra
NAT : Natural numbers (e.g. 26)
INT : Integers (e.g. -1)
RAT : Rational numbers (e.g. 1/3)
FLOAT : Floating numbers (e.g. 3.14159)
CHARACTER : Characters (e.g. 'A')
STRING : Strings (e.g. "abc")
QID : Quoted identifiers ('abc)
2TUPLE : 2-tuple
3TUPLE : 3-tuple
4TUPLE : 4-tuple
TRIV : The trivial module, which includes only the sort Elt and denotes a set.

Use the show command to show the detail of each built-in module:

[Next]