CafeOBJ examples

The examples are classified into five difficulty levels:

Level 1
- integer (ADT specification)
- list (ADT specification)
- natural number with addition and multiplication (ADT specification)
Level 2
- debt reduction algorithm (RWL specification)
- flag (behavioural specification)
- natural numbers with infinity (ADT specification)
- natural numbers with non-deterministic choice function (RWL specification)
- path data type featuring partial functions (ADT specification)
- telephone system (behavioural specification)
Level 3
- bag (behavioural specification)
- list (bahavioural specification)
- set (behavioural specification)
- counter (behavioural specification)
- counter with switch (behavioural specification)
- stack (behavioural specification)
- natural numbers with non-deterministic choice function (behavioural specification)
- Eratostene sieve algorithm (equational specification)
- watch (behavioural specification)
Level 4
- ATM (behavioural specification)
- bank account system (behavioural specification)
- generic sorting algorithm for string (RWL specification)
Level 5
- unreliable buffer (behavioural specification)