Next:The E-strategyUp:Operational Semantics of Rewriting Previous:Introduction

# Algebraic Specification Language CafeOBJ

CafeOBJ[2] is descended from OBJ[4,6], probably the most famous algebraic specification language. Although CafeOBJ provides many fascinating features and functionalities, we here take up only a few of them that are needed for writing the operational semantics of rewriting. One of them is the powerful module system inherited from OBJ. Modules can have parameters and import other modules. We give a parameterized module LIST as an example.

Example 1 (A parameterized module List).
mod! LIST (DAT :: TRIV) {
pr( NAT )
[ List ]
op nil : -> List
op _ _ : Elt.DATList -> List { r-assoc }
op _++_ : ListList -> List
op take : ListM/i> Nat -> Elt.DAT
op replace : ListNat Elt.DAT -> List
vars E E1 : Elt.DAT
vars L L1 : List
eq nil ++ L1 = L1 .
eq (E L) ++ L1 = E (L ++ L1) .
eq take(E L, 0) = E .
eqtake(E L, X:NzNat) = take(L, sd(X, 1)) .
eq replace(E L, 0, E1) = E1 L .
eq replace = (E L, X:NzNat, E1) = E replace(L, sd(X, 1), E1) .
}

A module (declaration) begins with the keyword mod! or mod* (which corresponds to tight or loose denotation), and has its name ( LIST in this example) and a list of parameters if exist (( DAT :: TRIV) in this example) after the keyword. A parameter consists of a parameter name ( DAT in this example) and a module name ( TRIV in this example). The module name describes requirements that the actual parameters must meet. The module body is enclosed by braces. The module body consists of some declarations such as import, sort, operator, variable and/or equation declarations.

The module LIST imports the built-in module NAT with protecting (abbr. pr) mode that requires all the intended models of imported modules ( NAT in this example) be preserved as they are (i.e. no junk and no confusion). There are two more importation modes: extending (abbr. ex) and using (abbr. us) modes. The ex mode allows the models of imported modules to be inflated, but does not allow them to be collapsed (i.e. no junk). The us mode imposes nothing on the models of imported modules. The built-in module BOOL, in which true, false and some logical operators are declared, is implicitly imported into any module by default.

LIST declares a new sort List. Sorts in algebraic specification languages may correspond to types in programming languages.

Operator declarations begin with op or ops and have the name, the sorts of the arguments and the sort of the result. They may have some attributes such as r-assoc meaning that the operator is right associative. Some operators such as nil have no arguments and are called constants. CafeOBJ makes it possible to declare not only standard operators such as f and g in f(g(1),2), but also mixfix operators such as _++_ (i.e. infix ones) and _ _ (i.e. juxtaposition ones). Underbars reserve the places where arguments are inserted.

Variable declarations begin with var or vars, and have the name and its sort. Sorts may be quantified by modules such as Elt. DAT. Variables may be declared in equation declarations such as X: NzNat.

Equation declarations begin with eq or ceq and end with a full stop. Conditional equations are declared with ceq.

An instance of parameterised modules is created by binding actual parameters to formals. The process of binding is called instantiation. The result of instantiation is a new module. For example, when LIST is instantiated by binding NAT to TRIV, we write LIST( NAT ). When instantiating the module LIST, it is also possible to rename the sort List another such as NatList by writing LIST( NAT )*{ sort List -> NatList }.

CafeOBJ specifications may be executed by regarding equations as left-to-right rewrite rules by a rewrite engine. Thanks to the executability, we can observe the dynamic behavior of rewriting with the on-demand E-strategy using the formal operational semantics in CafeOBJ.

Next:The E-strategyUp:Operational Semantics of Rewriting Previous:Introduction

Kazuhiro Ogata

Mon Nov 29 13:47:22 JST 1999