• Nonterminating CafeOBJ example (PDF)
• Nonconfluent CafeOBJ example (PDF)
• CafeOBJ rewriting options (PDF)
• Additional CafeOBJ facilities (PDF)
• Z vs. algebraic specification (PDF)
• Statechart preamble (PDF)
• Finite State Machines 2 by Douglas (PDF)