|
CafeOBJ exmaples
In the following examples, you may find "Chapter xx" in their explanations.
It corresponds to the text
"Introducing CafeOBJ" (in Japanese),
however, you may read and try those examples without the text.
Introductory Examples
- Introduction to CafeOBJ
- Tutorial site for beginners
- Examples of simple specifications
- Abstract data types: natural numbers, integers, bags (multiset)
- Observational transition systems (bahavioral specifications): arrays with an example of simple verification
- Other examples
- including abstract data types, rewrite specifications, behavioral specifications.
Examples of proof scores
- Vefification of Qlock protocol
- A specification of Qlock protocol with proof socre for some invariant properties. An introductory example of proof scores
- Verification of an Authentication Protocol
- A specification of NSLPK authentication protocol with proof socre for some invariant properties.
- Verification of a Communication Protocol
- A specification of SCP communication protocol with proof socre for some invariant properties.
|
|
|
