Specification and Verification of Software with CafeOBJ - Part 4 - Modules

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

In the last part we have made our first steps with CafeOBJ, learned how start and quit the interpreter, how to access the help system, and how to write basic functions. This time we will turn our attention to the most fundamental building blocks of specifications, modules.

But before diving into modules, let us give answers to the challenge posed at the end of the last blog, namely to give definitions of the factorial function and the Fibonacci function. Without much discussion, here is the one possible solution for the Fibonacci numbers:

-- Factorial
open NAT .
op _! : Nat -> Nat .
eq 0 ! = 1 .
eq ( X:NzNat ! ) = X * ( (p X) ! ) .
red 10 ! .
close
-- Fibonacci
open NAT .
op fib : Nat -> Nat .
eq fib ( 0 ) = 0 .
eq fib ( 1 ) = 1 .
ceq fib ( X:Nat ) = fib (p X) + fib (p (p X)) if X > 1 .
red fib(10) .
close

Note that in the case of factorial we used the standard mathematical notation of postfix bang. We will come to the allowed syntax later on.

Modules

Modules are the basic building blocks of CafeOBJ specifications, and they correspond - or define - order-sorted algebras. Think about modules as a set of elements, operators on these elements, and rules how they behave. A very simple example of such a module is:

module ADDMOD {
[ Elem ]
op _+_ : Elem Elem -> Elem .
op 0 : -> Elem .
eq 0 + A:Elem = A .
}

This modules is introduced using the keyword module and the identifier ADDMOD, and the definition is enclosed in curly braces. The first line [ Elem ] defines the types (or sorts) available in the module. Most algebra one sees is mono-sorted, so there is only one possible sort, but algebras in CafeOBJ are many-sorted, and in fact order-sorted (we come to that later). So the module we are defining contains only elements of one sort Elem.

Next up are two lines starting with op, which introduces operators. Operators (think "functions") have a certain arity, that is, the take a certain number of arguments and return a value. In the many-sorted case we not only need to specify how many arguments an operator takes, but also from which sorts these arguments are. In the above case, let us first look at the line op _+_ : Elem Elem -> Elem .. Here an infix operator + is introduced, that takes two arguments of sort Elem, and returns again an Elem.

The next line defines an operator 0 - you might ask what a strange operator this is, but looking at the definition we see that there is no arguments to the operator, only a result. This is the standard way to define constants. So we now have an addition operator and a constant operator.

The last line of the definition starts with eq which introduces an equality, or axiom, or rule. It states that the left side and the right side are equal, in mathematical terms, that 0 is a left-neutral element of +.

Even with much more complicated modules, these three blocks will form most of the code one writes in CafeOBj: sort declarations, operator declarations, axiom definitions.

A first module

Let us define a bit more involved module extending the ideas of the pet example above:

mod! PNAT {
[ PNat ]
op 0 : -> PNat .
op s : PNat -> PNat .
op _+_ : PNat PNat -> PNat .
vars X Y : PNat
eq 0 + Y = Y .
eq s(X) + Y = s(X + Y) .
}

You will immediately recognize the same parts as in the first example, sort declaration, three operator declarations, and two axioms. There are two things that are new: (1) the module started with mod!: mod is a shorthand for the longer module, and the bang after it indicates that we are considering initial models - we wont go into details about initial versus free models here, though; (2) the line vars X Y : PNat: we have seen variable declarations inline in the first example A:Elem, but instead of this inline definition of variables one can defines variables beforehand and use them later on multiple times.

For those with mathematical background, you might have recognized that the name of the module (PNAT) relates to the fact that we are defining Peano Natural Numbers here. For those with even more mathematical background - yes I know this is not the full definition of Peano numbers ;-)

Next, let us see what we can do with this module, in particular what are elements of this algebra and how we can add them. From the definiton we only see that 0 is a constant of the algebra, and that the monadic operator s defines new elements. That means, that terms of the form 0, s(0), s(s(0)), s(s(s(0))) etc are PNats (not ). So, can we do computations with these kind of numbers? Let us see:

CafeOBJ> open PNAT .
-- opening module PNAT.. done.
%PNAT> red s(s(s(0))) + s(s(0)) .
-- reduce in %PNAT : (s(s(s(0))) + s(s(0))):PNat
(s(s(s(s(s(0)))))):PNat
(0.0000 sec for parse, 0.0010 sec for 4 rewrites + 7 matches)
%PNAT> close
CafeOBJ>

Oh, CafeOBJ computed something for us. Let us look into details of the computation. CafeOBJ has a built-in tracing facility that shows each computations step. It is activated using the code set trace whole on:

%PNAT> set trace whole on

%PNAT> red s(s(s(0))) + s(s(0)) .
-- reduce in %PNAT : (s(s(s(0))) + s(s(0))):PNat
[1]: (s(s(s(0))) + s(s(0))):PNat
---> (s((s(s(0)) + s(s(0))))):PNat
[2]: (s((s(s(0)) + s(s(0))))):PNat
---> (s(s((s(0) + s(s(0)))))):PNat
[3]: (s(s((s(0) + s(s(0)))))):PNat
---> (s(s(s((0 + s(s(0))))))):PNat
[4]: (s(s(s((0 + s(s(0))))))):PNat
---> (s(s(s(s(s(0)))))):PNat
(s(s(s(s(s(0)))))):PNat
(0.0000 sec for parse, 0.0000 sec for 4 rewrites + 7 matches)

The above trace shows that the rule (axiom) eq s(X) + Y = s(X + Y) . is applied from left to right until the final term is obtained.

The underlying computation mechanism of CafeOBJ is Term Rewriting, in particular order-sorted conditional term rewriting with associativity and commutativity (AC). Just as a side node, CafeOBJ is one of the very few (if not the only one still in use) system that implements conditional AC rewriting, in addition on order-sorted terms.

We wont go into details of the intricacies of term rewriting but mention only one thing that is important for the understanding of the computational model of the CafeOBJ interpreter: While axioms (equations) do not have a direction, they are just statements of equality between two terms, the evaluation carried out by the red uses the axioms only in the direction from left to right, thus it is important how an equation is written down. General rule is to write the complex term on the left side and the simple term on the right (if it is easy to define what is the more complex one).

Let us exhibit this directional usage on a simple example. Look at the following code, what will happen?

mod! FOO {
[ Elem ]
op f : Elem -> Elem .
op a : -> Elem .
var x : Elem
eq f(x) = f(f(x)) .
}
set trace whole on
open FOO .
red f(a) .

I hope you guessed it, we will send CafeOBJ into an infinite loop:

%FOO> red f(a) .
-- reduce in %FOO : (f(a)):Elem
[1]: (f(a)):Elem
---> (f(f(a))):Elem
[2]: (f(f(a))):Elem
---> (f(f(f(a)))):Elem
[3]: (f(f(f(a)))):Elem
---> (f(f(f(f(a))))):Elem
[4]: (f(f(f(f(a))))):Elem
...

This is because the rules are strictly applied from left to right, and this can be done again and again.

To close this blog, let us use modules to define a very simple list of natural numbers: A list can either be empty, or it is a natural number followed by the symbol | and another list. In BNF this would look like

L ::= nil | x|L

Some examples of list and things that are not proper lists:
　・nil - this is a list, the most simple one
　・1 | ( 3 | ( 2 | nil ) ) - again a list, with all parenthesis
　・1 | 3 | 2 | nil - again a list, if we assume right associativity of |
　・1 | 3 | 2 - not a list, because the last element is a natural number and not a list
　・(1 | 3) | 2 | nil - again not a list, because the first element is not a natural number
Now let us reformulate this in CafeOBJ language:

mod! NATLIST {
pr(NAT)
[ NatList ]
op nil : -> NatList .
op _|_ : Nat NatList -> NatList .
}

Here one new syntax element did appear: the line pr(NAT) which is used to pull in the natural numbers NATin a protected way pr. This is the general method to include other modules and build up more complex entities. We will discuss import methods later on.

We also see that within the module NATLIST we have now multiple sorts (Nat and NatList, and operators that take arguments of different sorts.

As a final step, let us see whether the above definition is consistent with our list intuition from above, i.e., that the CafeOBJ parser accepts exactly these terms. We can use the already known red here, but if we only want to check whether an expression can be correctly parsed, CafeOBJ also offers the parse command. Let us use it to check the above list:

CafeOBJ> open NATLIST .

%NATLIST> parse nil .,

(nil):NatList

%NATLIST> parse 1 | ( 3 | ( 2 | nil ) ) .

(1 | (3 | (2 | nil))):NatList

%NATLIST> parse 1 | 3 | 2 | nil .

(1 | (3 | (2 | nil))):NatList

%NATLIST>

Up to here, all fine, all the terms we hoped that they are lists are properly parsed into NatList. Let us try the same with the two terms which should not be parsed correctly:

%NATLIST> parse 1 | 3 | 2 .

[Error]: no successful parse
(parsed:[ 1 ], rest:[ (| 3 | 2) ]):SyntaxErr

%NATLIST> parse (1 | 3) | 2 | nil .

[Error]: no successful parse
((( 1 | 3 ) | 2 | nil)):SyntaxErr

As we see, parsing did not succeed, which is what we expected. CafeOBJ also tells us up to which part the parsing did work out, and where the first syntax error did occur.

This concludes the introduction to modules. Let us conclude with a challenge for the interested reader.

Enrich the NatList module with an operator len that computes the length of a list. Here is the basic skeleton to be filled in:

op len : NatList -> Nat .
eq len(nil) = ??? .
eq len(E:Nat | L:NatList) = ??? .

Test your code by looking at the rewriting trace.


■関連ページ
【アクセリアのサービス一覧】
　・サービスNAVI