仕様の記述

CafeOBJ の仕様は、拡張子 .mod を持つテキストファイルとして記述する。

以下に自然数の仕様を記述した CafeOBJ の仕様の例を示す。

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

今は仕様が表す意味が理解できなくてもかまわない。

上記の仕様を、simple-nat.mod というファイル名を付けて保存せよ。ファイルは、任意のディレクトリに置いてかまわない。上記の仕様を手入力する場合は、キーワードの間に空白が必要な箇所があること、および CafeOBJ はキーワードに含まれる大文字小文字を厳格に区別することに注意せよ。

[Next] 仕様の読み込み

Original Copyright © Takahiro Seino, all rights reserved.