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

Exercises

Exercise 1

Complete a proof score of the commutativity of + in NAT+.

Exercise 2

After finishing the proofs of the associativity and the commutativity of +, those properties can be declared by adding to the attribute assoc comm to +. Consider the following modules:

mod! NAT+AC {
  pr(NAT+)
  op _+_ : Nat Nat -> Nat { assoc comm }
}

mod! NAT* {
  pr(NAT+AC)
  op _*_ : Nat Nat -> Nat
  eq 0 * M:Nat = 0 .
  eq s(N:Nat) * M:Nat = M + (N * M) .
}

Prove the distributive law, that is, i * (j + k) = (i * j) + (i * k) in NAT*.

Exercise 3

Consider why NAT+AC does not include equations of the associative and the commutative laws instead of the attributes. What kinds of trouble happen in the following module?

mod! NAT+AC2 {
  pr(NAT+)
  -- associativity on _+_
  eq (I:Nat + J:Nat) + K:Nat = I + (J + K) .
  -- commutativity on _+_
  eq I:Nat + J:Nat = J + I .
}

[Next]