Introduction

This is a brief introduction to CafeOBJ for beginners. The main purpose of this introduction is to experience how to do formal methods with CafeOBJ from description to verification through a simple example of natural numbers.

This document is organized as follows:

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

History


Original Copyright © Takahiro Seino, all rights reserved.