# Specification and Verification of Software with CafeOBJ – Part 3 – First steps with CafeOBJ

This blog continues Part 1 and Part 2 of our series on software specification and verification with CafeOBJ.

We will go through basic operations like starting and stopping the CafeOBJ interpreter, getting help, doing basic computations.

## Starting and leaving the interpreter

If CafeOBJ is properly installed, a call to `cafeobj`

will greet you with information about the current version of CafeOBJ, as well as build dates and which build system has been used. The following is what is shown on my Debian system with the latest version of CafeOBJ installed:

$ cafeobj -- loading standard prelude -- CafeOBJ system Version 1.5.7(PigNose0.99) -- built: 2018 Feb 26 Mon 6:01:31 GMT prelude file: std.bin *** 2018 Apr 19 Thu 2:20:40 GMT Type ? for help *** -- Containing PigNose Extensions -- --- built on SBCL 1.4.4.debian CafeOBJ> |

After the initial information there is the prompt `CafeOBJ>`

indicating that the interpreter is ready to process your input. By default several files (the *prelude* as it is called above) is loaded, which defines certain basic sorts and operations.

If you have enough of playing around, simply press `Ctrl-D`

(the `Control`

key and `d`

at the same time), or type in `quit`

:

CafeOB> quit $ |

## Getting help

Besides the extensive documentation available at the website (reference manual, user manual, tutorials, etc), the reference manual is also always at your fingertips within the CafeOBJ interpreter using the `?`

group of commands:

`?`

– gives general help`?com class`

– shows available commands classified by ‘class’`? name`

– gives the reference manual entry for*name*`?ex name`

– gives examples (if available) for*name*`?ap name`

– (apropos) searches the reference manual for appearances of*name*

To give an example on the usage, let us search for the term *operator* and then look at the documentation concerning one of them:

CafeOBJ> ?ap op Found the following matches: . `:theory <op_name> : <arity> -> <coarity> { assoc | comm | id: <term> }` ... . `op <op-spec> : <sorts> -> <sort> { <attribute-list> }` . on-the-fly declaration ... CafeOBJ> ? op `op <op-spec> : <sorts> -> <sort> { <attribute-list> }` Defines an operator by its domain, co-domain, and the term construct. `<sorts>` is a space separated list of sort names, `<sort>` is a single sort name. ... |

I have shortened the output a bit indicated by `...`

.

## Simple computations

By default, CafeOBJ is just a barren landscape, meaning that there are now rules or axioms active. Everything is encapsulated into so called *modules* (which in mathematical terms are definitions of order-sorted algebras). One of these modules is `NAT`

which allows computations in the natural numbers. To activate a module we use `open`

:

CafeOBJ> open NAT . ... %NAT> |

The `...`

again indicate quite some output of the CafeOBJ interpreter loading additional files.

There are two things to note in the above:

- One finishes a command with a literal dot
`.`

– this is necessary due to the complete free syntax of the CafeOBJ language and indicates the end of a statement, similar to semicolons in other programming languages. - The prompt has changed to
`NAT>`

to indicate that the playground (context) we are currently working are the natural numbers.

To actually carry out computations we use the command `red`

or `reduce`

. Recall from the previous post that the computational model of CafeOBJ is rewriting, and in this setting reduce means kicking of the rewrite process. Let us do this for a simple computation:

%NAT>; red 2 + 3 * 4 . -- reduce in %NAT : (2 + (3 * 4)):NzNat (14):NzNat (0.0000 sec for parse, 0.0000 sec for 2 rewrites + 2 matches) %NAT> |

Things to note in the above output:

- Correct operator precedence: CafeOBJ correctly computes 14 due to the proper use of operator precedence. If you want to override the parsing you can use additional parenthesis.
- CafeOBJ even gives a sort (or type) information for the return value:
`(14):NzNat`

, indicating that the return value of 14 is of sort`NzNat`

, which refers to*non-zero natural numbers*. - The interpreter tells you how much time it spent in parsing and rewriting.

If we have enough of this playground, we close the opened module with `close`

which returns us to the original prompt:

%NAT> close . CafeOBJ> |

Now if you think this is not so interesting, let us to some more funny things, like computation with rational numbers, which are provided by CafeOBJ in the `RAT`

module. Rational numbers can be written as *slashed expressions*: `a / b`

. If we don’t want to actually reduce a given expression, we can use `parse`

to tell CafeOBJ to parse the next expression and give us the parsed expression together with a sort:

CafeOBJ> open RAT . ... %RAT> parse 3/4 . (3/4):NzRat %RAT> |

Again, CafeOBJ correctly determined that the given value is a non-zero rational number. More complex expression can be parsed the same way, as well as reduced to minimal representation:

%RAT> parse 2 / ( 4 * 3 ) . (2 / (4 * 3)):NzRat %RAT> red 2 / ( 4 * 3 ) . -- reduce in %RAT : (2 / (4 * 3)):NzRat (1/6):NzRat (0.0000 sec for parse, 0.0000 sec for 2 rewrites + 2 matches) %RAT> |

`NAT`

and `RAT`

are not the only built-in sorts, there are several more, and others can be defined easily (see next blog). The currently available data types, together with their sort order (recall that we are in order sorted algebras, so one sort can contain others):

`NzNat < Nat < NzInt < Int < NzRat < Rat`

which refer to non-zero natural numbers, natural numbers, non-zero integers, integers, non-zero rational numbers, rational numbers, respectively.

Then there are other data types unrelated (not ordered) to any other:

`Triv`

, `Bool`

, `Float`

, `Char`

, `String`

, `2Tuple`

, `3Tuple`

, `4Tuple`

.

## Functions

CafeOBJ does not have functions in the usual sense, but *operators* defined via there arity and a set of (rewriting) equations. Let us take a look at two simple functions in the natural numbers: `square`

which takes one argument and returns the square of it, and a function `sos`

which takes two arguments and returns the sum of squares of the arguments. In mathematical writing: `square(a) = a * a`

and `sos(a,b) = a*a + b*b`

.

This can be translated into CafeOBJ code as follows (from now on I will be leaving out the prompts):

open NAT . vars A B : Nat op square : Nat -> Nat . eq square(A) = A * A . op sos : Nat Nat -> Nat . eq sos(A, B) = A * A + B * B . |

This first declares two variables A and B to be of sort `Nat`

(note that the module names and sort names are not the same, but the module names are usually the uppercase of the sort names). Then the operator `square`

is introduced by providing its arity. In general an operator can have several input variables, and for each of them as well as the return value we have to provide the sorts:

op NAME : Sort1 Sort2 ... -> Sort |

defines an operator `NAME`

with several input parameters of the given sorts, and the return sort `Sort`

.

The next line gives one (the only necessary) equation governing the computation rules of `square`

. Equations are introduced by `eq`

(and some variants of it), followed by an expression, and equal sign, and another expression. This indicates that CafeOBJ may rewrite the left expression to the right expression.

In our case we told CafeOBJ that it may rewrite an expression of the form `square(A)`

to `A * A`

, where `A`

can be anything of sort `Nat`

(for now we don't go into details how order-sorted rewriting works in general).

The next two lines do the same for the operator `sos`

.

Having this code in place, we can easily do computations with it by using the already introduced `reduce`

command:

red square(1) . -- reduce in %NAT : (square(10)):Nat (100):NzNat red sos(10,20) . -- reduce in %NAT : (f(10,20)):Nat (500):NzNat |

What to do if one equation does not service? Let us look at a typical recursive definition of *sum* of natural numbers: `sum(0) = 0`

and for `a > 0`

we have `sum(a) = a + sum(a-1)`

. This can be easily translated into CafeOBJ as follows:

open NAT . op sum : Nat -> Nat . eq sum(0) = 0 . eq sum(A:NzNat) = A + sum(p A) . red sum(10) . |

where `p`

(for *predecessor*) indicates the next smaller natural number. This operator is only defined on non-zero natural numbers, though.

In the above fragment we also see a new style of declaring variables, *on the fly*: The first occurrence of a variable in an equation can carry a sort declaration, which extends all through the equation.

Running the above code we get, not surprisingly 55, in particular:

-- reduce in %NAT : (sum(10)):Nat (55):NzNat (0.0000 sec for parse, 0.0000 sec for 31 rewrites + 41 matches) |

As a challenge the reader might try to give definitions of the factorial function and the Fibonacci function, the next blog will present solutions for it.

This concludes the second part. In the next part we will look at defining modules (aka algebras aka theories) and use them to define lists.

What always bugged me and prevented me into diving into CafeOBJ further (well not that I would really have time nowadays, but still) is that there is no textbook-like intro into the mathematical foundations of CafeOBJ. Like Nipkow’s “Term Rewriting Systems”, written for a master student without assuming prior knowledge of many of these things. I mean algebras, ok, rewriting, ok, but hidden algebra? Behavioral operations?? Cobases??? It’s really hard to actually _use_ CafeOBJ for proofs, if you don’t know the inherent limitations of modeling; and don’t have time to read a bazillion of ancient papers by Goguen and stuff…