Norbert Preining氏による【Specification and Verification of Software with CafeOBJ -Part 3】を公開

「Starting and leaving the interpreter」
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.

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:

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 ? 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.


・・・ここから先は、アクセリア株式会社で公開中のコラム本編でご覧ください。
リンク


【アクセリア株式会社の研究開発部社員：Norbert Preining氏のコラム】
・第1回：今さら聞けない、機械学習/ディープラーニングとは！？リンク
・第2回：最新の機械学習の代表、ニューラルネットワークとはリンク
・第3回：手書き数字を認識する機械学習リンク
・第4回：畳み込みニューラルネットワークリンク
・第5回：機械学習における今後の展開リンク
・第9回：Analyzing Debian packages with Neo4jリンク
・第10回：Analyzing Debian packages with Neo4j - Part 2 UDD and Graph DB Schemaリンク
・第11回：Analyzing Debian packages with Neo4j - Part 3 Getting data from UDD into Neo4jリンク
・第12回：Specification and Verification of Software with CafeOBJ - Part 1 - Introducing CafeOBJリンク
・第13回：Specification and Verification of Software with CafeOBJ - Part 2 - Basics of CafeOBJリンク


【アクセリア株式会社の研究開発部社員のコラム】
・第6回：アクセリアが手がけるP2P (Peer-to-Peer)リンク
・第7回：効率的な検索を可能にする、グラフデータベースリンク
・第8回：アクセリアにおけるディープラーニング適用例リンク