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
- 2009-12-01 Open English version. Thanks for Dr. Masaki Nakamura's contribution.
[Next] Start and Quit
Original Copyright © Takahiro Seino, all rights reserved.