Specification and Verification of Software with CafeOBJ - Part 3 - First steps with CafeOBJ

Starting and leaving the interpreter
This blog continues Part 1 and Part 2 of our series on software specification and verification with CafeOBJ.
(Part 1 and Part 2)
We will go through basic operations like starting and stopping the CafeOBJ interpreter, getting help, doing basic computations.
If CafeOBJ is properly installed, a call to
After the initial information there is the prompt
If you have enough of playing around, simply press
(Part 1 and Part 2)
We will go through basic operations like starting and stopping the CafeOBJ interpreter, getting help, doing basic computations.
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.debianCafeOBJ>
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
:
CafeOBJ> 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
・
・
・
・
・
To give an example on the usage, let us search for the term operator and then look at the documentation concerning one of them:
I have shortened the output a bit indicated by
?
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 nameTo 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
The
There are two things to note in the above:
・One finishes a command with a literal dot
syntax of the CafeOBJ language and indicates the end of a statement, similar to semicolons
in other programming languages.
・The prompt has changed to
currently working are the natural numbers.
To actually carry out computations we use the command
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:
that the return value of 14 is of sort
・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
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
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:
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:
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 arecurrently 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
, indicatingthat 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:
This can be translated into CafeOBJ code as follows (from now on I will be leaving out the prompts):
This first declares two variables A and B to be of sort
defines an operator
The next line gives one (the only necessary) equation governing the computation rules of
In our case we told CafeOBJ that it may rewrite an expression of the form
The next two lines do the same for the operator
Having this code in place, we can easily do computations with it by using the already introduced
What to do if one equation does not service? Let us look at a typical recursive definition of sum of natural numbers:
where
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:
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.
■関連ページ
【アクセリアのサービス一覧】
・サービスNAVI
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.
■関連ページ
【アクセリアのサービス一覧】
・サービスNAVI
Contact usお問い合わせ
サービスにご興味をお持ちの方は
お気軽にお問い合わせください。
Webからお問い合わせ
お問い合わせお電話からお問い合わせ
03-5211-7750
平日09:30 〜 18:00
Free Service