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
- Verification with proof scores
- Proof scores
- Equality predicate
- Associativity of
- Commutativity of
- Built-in modules
- 2009-12-01 Open English version. Thanks for Dr. Masaki Nakamura's contribution.
Original Copyright © Takahiro Seino, all rights reserved.