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.


Original Copyright © Takahiro Seino, all rights reserved.