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

Imports

A module can import other modules. In the importing module, elements declared in the imported module can be used.

There are three kinds of import declarations: protecting, extending and using (or just pr, ex and us):

pr(<module-exp>)
ex(<module-exp>)
us(<module-exp>)

The name of a module to be imported is written in <module-exp>.

Each of pr, ex and us states to what extent the intended models of the imported modules are preserved within those of the importing modules.

pr : does not allow elements to be added and collapsed.
ex : allows elements to be added but does not allowed to be collapsed.
us : allows total destruction.

When importing NAT+ with ex, A new element nan can be added to Nat, however it is not allowed when the import mode is pr:

mod! NAT+NAN {
  ex(NAT+)
  op nan : -> Nat
}

When importing NAT+ with us, Terms s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) (=12) and 0 are allowed to be a same element. Then, a specification of arithmetic modulo 12 is obtained (*). This is not allowed when importing modules with pr or ex.

(*) In HOUR12, it holds that not only 12 = 0 but also 13 = 1, 14 = 2, and so on.

mod! HOUR12 {
  us(NAT+)
  eq s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) = 0 .
}

[Next] Operators