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

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

第13回:Specification and Verification of Software with CafeOBJ -Part 2 - Basics of CafeOBJ

「Availability of CafeOJB」
This blog continues Part 1リンク of our series on software specification and verification with CafeOBJ.

CafeOBJ can be obtained from the website cafeobj.org. The site provides binary packages built from Linux, MacOS, and Windows, as well as the source code for those who want to build the interpreter themselves. Other services provided are tutorial pages, all kind of documentation (reference manual, wiki, user manual).

「What is CafeOBJ」
Let us recall some of the items mentioned in the previous blog. CafeOBJ is an algebraic specification language, as well as a verification and programming language. This means, that specifications written in CafeOBJ can be verified right within the system without the need to regress to external utilities.

As algebraic specification language it is built upon the logical foundation formed by the following items: (i) order sorted algebras, (ii) co-algebras (or hidden algebras), and (iii) rewriting logic. As verification and programming language it provides the user with an executable semantics of the equational theory, a rewrite engine that supports conditional, order-sorted, AC (associative and commutative) rewriting, a sofisticated module system including parametrization and inheritance, and last but not least a completely free syntax.

The algebraic semantics can be represented by the CafeOBJ cube exhibiting the various extensions starting more many sorted algebras:

For the algebraically inclined audience we just mention that all the systems and morphisms are formalized as institutions and institution morphisms.Let us now go through some the the logical foundations of CafeOBJ:

「Term rewriting」
Term rewriting is concerned with systems of rules to replace certain parts of an expression with another expression. A very simple example of a rewrite system is:

 append(nil, ys) → ys
 append(x : xs, ys) → x : append(xs, ys)

Here the first rule says that you can rewrite an expression append(nil, ys) where ys can be any list, with ys itself. And the second rule states how to rewrite an expression when the first element is not the empty list.

A typical reduction sequence - that is application of these rules - would be:

append(1 ∶ 2 ∶ 3 ∶ nil, 4 ∶ 5 ∶ nil) → 1 ∶ append(2 ∶ 3 ∶ nil, 4 ∶ 5 ∶ nil)
                  → 1 ∶ 2 ∶ append(3 ∶ nil, 4 ∶ 5 ∶ nil)
                  → 1 ∶ 2 ∶ 3 ∶ append(nil, 4 ∶ 5 ∶ nil)
                  → 1 ∶ 2 ∶ 3 ∶ 4 ∶ 5 ∶ nil

Term rewriting is used in two different ways in CafeOBJ: First as execution engine that considers equations as directed rules and uses them to reduce expressions. And at the same time rewriting logic is included into the language specification allowing for reasoning about transitions.

「Order sorted algebras」
Most algebras we learn in school or even at the university are single sorted, that is all objects in the algebra are of the same type (e.g., integers, reals, function space). In this case an operation is determined by its arity, that is the number of arguments.

In the many sorted and order sorted case the simple number of arguments of a function is not enough, we need to know for each argument its type and also the type of the value the function returns. Thus, we assume a signature (S,F) given, such that S is a set of sorts, or simply sort names, and F is a set of operations f: s1, s2, ..., sk → s where all the s are sorts.

As an example assume we have two sorts, String and Int, one possible function would be

 substr: String, Int, Int → String

which would tell us that the function substr takes three arguments, the first of sort String, the others of sort Int, and it returns again a value of sort String.

In case the sorts are (partially ordered), we call the corresponding algebra order sorted algebra.

Using order sorted algebras has several advantages compared to other algebraic systems:

 ・polymorphism (parametric, subsort) and overloading are natural consequences of ordered sorts;
 ・error definition and handling via subsorts;
 ・multiple inheritance;
 ・rigorous model-theoretic semantics based on institutions;
 ・operational semantics that executes equations as rewrite rules (executable specifications).

We want to close this blog post with a short history of CafeOBJ and a short sample list of specifications that have been carried out with CafeOBJ.


【アクセリア株式会社の研究開発部社員: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リンク

・第6回:アクセリアが手がけるP2P (Peer-to-Peer)リンク


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