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

アクセリア株式会社の研究開発部社員であるNorbert Preining氏による、コラム連載を開始しました。 https://www.accelia.net/column/research/

第14回: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.

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

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 .

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
(0.0000 sec for parse, 0.0000 sec for 2 rewrites + 2 matches)


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 .

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 .

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
(0.0000 sec for parse, 0.0000 sec for 2 rewrites + 2 matches)


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氏のコラム】
・第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)リンク


このサイトでは、利用状況の把握や広告配信などのために、Cookieなどを使用してアクセスデータを取得・利用しています。 これ以降ページを遷移した場合、Cookieなどの設定や使用に同意したことになります。
[ 閉じる ]