Overview of OBJ3

We present a brief account of the main features of OBJ3 and how these features relate to Axis. We do not aim to provide an exhaustive manual of the OBJ3 programming language here - for more details the reader is referred to [Goguen and Winkler 88]. OBJ3 is a wide spectrum programming language which consists of an interpreter and an environment for a powerful functional programming language. It has a rigorous mathematical semantics based on order-sorted equational logic. This logic uses the concept of subsorts which provides a simple, yet mathematically precise way of handling errors and operation overloading.

The rigorous semantics allows specifications to be written as programs which are declarative in style and which mirror the structure of an algebraic specification. This permits OBJ3 to be used not only for validating and implementing algebraic specifications but also as a theorem prover. The three top-level programming structures which support the specification of abstract data types are object modules, theory modules and views.

• objects : these encapsulate executable code and correspond to the SPEC modules of Axis. They are delimited by the keywords obj and endo which correspond to our SPEC and ENDSPEC respectively.
• theories : these define the syntax and semantic properties of modules and module interfaces. They specify properties that may (or may not) be satisfied by another object or theory. They are structurally similar to object modules in that they consist of a collection of sorts, subsorts, operations, variable declarations and axioms (not necessarily all), but they do not enforce an initial interpretation. These correspond to the PROPS modules of Axis.
• views : these are a concept we discussed in the context of parameterised specifications in chapter 11 (section 11.9). We recall that a view is a binding between the sorts and/or operations declared in some theory to sorts and/or operations in some other module together with an assertion that this other module satisfies the properties stated in the theory. Views are delimited by the keywords view and endv.

As with Axis, both types of module (object and theory) can be parameterised where the parameter types are modules. Modules can also import existing modules which supports multiple inheritance at the module level. Large specifications can then be built up in bottom-up fashion using module expressions which consist of unparameterised object modules, instantiated parameterised modules, renamed modules and the sum combinator operator (+), in much the same way as discussed in chapter 11.

With regards to the importing of modules, OBJ3 handles this feature differently from Axis. Whereas Axis identifies two ways that modules can be imported, namely USING which preserves the initial semantics of the imported module and INCLUDING which guarantees nothing, OBJ3 provides three means for importing modules, protecting, extending and using. The meanings of these types of import is connected with the initial semantics of objects as described below. Assume that a module S imports a module T. The importation is

(1) protecting if and only if S adds no new data values of sorts from T and does not force two distinct values of T to be equal. In other words, S does not introduce junk or confusion. This is equivalent to the USING construct of Axis.

(2) extending if and only if the axioms of S do not force two distinct values of T to be equal. In other words, the enlarged specification preserves the ``no confusion'' property. This type of importation has no equivalent in Axis.

(3) using if there are no guarantees at all. This is equivalent to our INCLUDING construct.

OBJ3 has a built-in binary infix equality operation _ == _ : S S -> Bool for every sort S and also has a number of built-in pre-defined data types such as BOOL, NAT, INT, FLOAT corresponding to the theory of Boolean values, natural numbers, integers and floating point values respectively. The polymorphic function if _ then _ else _ fi is provided by BOOL.

The axioms of an OBJ3 specification are referred to as equations and are prefixed by one of the keywords eq or cq which denotes an unconditional or conditional axiom respectively. Also OBJ3 supports prefix, postfix, infix and mixfix syntax for operations, in addition to the mathematical parenthesised prefix form. The reader should be aware of the terminology used in OBJ3 for the domain and range sorts of an operation. Given an operation op

op : s1 s2 ...sn     ->     s

the domain ${\tt s1 \enskip \times \enskip s2 \enskip \times \enskip \dots \enskip \times \enskip sn}$ is known as the arity and the range sort s is known as the value sort or co-arity. The pair (arity, co-arity) is called the rank of an operation. OBJ3 employs the convention that an expression is well-formed if and only if it has a unique parse of least sort. One further distinguishing feature of OBJ3 is its use of retracts to parse terms which on first inspection look as though they are not well-formed. When subterms are not of the anticipated sort, they can sometimes be coerced to that sort and this is a simple task from a subsort to a supersort. For instance, consider the two sorts Nat and Rat corresponding to the sorts of natural numbers and rational numbers respectively. Suppose the addition operation _ + _ : Rat Rat -> Rat is only defined over the rational numbers, then 1 + 2 can be made to conform to the pattern laid down by that signature because 1 and 2 are natural numbers and Nat < Rat, that is the sort of natural numbers is a subsort of the sort of rationals. Put another way, any natural number can be represented as a rational. For example, 1 + 2 can be expressed as 1/1 + 2/1 and so conforms to the signature of the original operation +.

Coercions from supersorts to subsorts are more subtle, however, and one distinguishing feature of OBJ3 is its use of retracts to handle such coercions. As an illustration, suppose the factorial function is defined for natural numbers only, and that the parser is presented with the expression (-6/-3)!. The parser must treat the subterm -6/-3 (which is strictly a rational) as a natural number since at parse time it cannot ascertain whether -6/-3 will evaluate to a natural number. In OBJ3, such subterms are ``given extra breathing space'' by having the parser introduce a retract which for this example is denoted by the special operation symbol r:Rat>Nat. The effect of a retract is to lower the sort and the retract is then withdrawn if the subterm evaluates to a natural number. In the event of the subterm not evaluating to a natural number, the retract is left behind where it then serves as an instructive error message. For our example, the parser will transform the expression (-6/-3)! into the expression (r:Rat>Nat(-6/-3))! which at run-time first evaluates to (r:Rat>Nat(2))! and subsequently (2)! using the built-in equation r:Rat>Nat(X) = X where X is any variable which belongs to Nat.

Finally, the period character `` . '' is somewhat special in OBJ3 as it used to terminate operation, variable and axiom declarations among other duties. Care has to be taken when using periods in any other context, for example as an operation symbol, since the interpreter will think a ``loose'' period within an axiom denotes the end of the axiom. OBJ3 is very tetchy on this point as the authors discovered to their cost when prototyping some of the specifications. Expeditious use of brackets is the order of the day in these situations !

We conclude this summary with a specimen OBJ3 program for a parameterised queue module. The requirement theory is ELEM which simply requires the existence of a sort and corresponds exactly to our PROPS module Elem given in Fig. 11.14. The parameterised specification is then instantiated to produce a specification for a queue of natural numbers. The resulting program is shown in Fig. 13.1. Observe that we have chosen to write the accessor operations in prefix form while the constructors are expressed in parenthesised prefix format. This is done merely to display the features of OBJ3 and is no requirement of OBJ3 itself. Note also that comments in OBJ3 are introduced by ***> or ***. The former print during execution while the latter do not.

  

Figure 13.1: Specification of a generic queue using OBJ3

We can then instantiate the formal parameter E with the (built-in) module NAT to produce a specification of a queue of natural numbers. We rename the sorts and the accessor operations to reflect this application and the resulting specification is shown below.

   obj  QUEUE-OF-NAT  is

      protecting  QUEUE[NAT]  *

                    ( sort  Queue      to  QueueNat ,

                      sort  NeQueue    to  NeQueueNat ,

                      op  front _      to  first _ ,

                      op  is-empty? _  to  empty-queue? _ ) .

   endo

We have used a default view in the instantiation QUEUE[NAT] which is equivalent to the explicitly stated form

QUEUE[view to NAT is sort Element to Nat . endv]

where Nat is the sort corresponding to the built-in module NAT.

Given an object (specification module) together with an expression <Expr>, (the input to the prototype program) the expression can be evaluated (that is reduced by applying an appropriate sequence of axioms in the form of rewrite rules) by using the command

reduce <Expr> .

and such an expression is evaluated with respect to the last module entered into the system. If it is required to reduce an expression with respect to a different module <ModName>say, the appropriate command is

reduce in <ModName> : <Expr> .

As an example, evaluation of the expression

first add(add(new, 2), 9)

is accomplished by the command

reduce in QUEUE-OF-NAT : first add(add(new, 2), 9) .

and the corresponding output from this program is

reduce in QUEUE-OF-NAT : first add(add(new,2),9) 
rewrites: 6
result NzNat: 2

where NzNat denotes the type (sort) of the result, a non-zero natural number.

Similarly, to find the canonical form of the term remove(add(add(new, 1), 4)), use the command

reduce in QUEUE-OF-NAT : remove(add(add(new, 1), 4)) .

which produces the result

reduce in QUEUE-OF-NAT : remove(add(add(new,1),4)) 
rewrites: 6
result NeQueueNat: add(new,4)

To determine whether two ground terms are equal, say for example the terms
remove(add(add(new, 1), 4)) and add(new, 4), we use the command

reduce in QUEUE-OF-NAT : remove(add(add(new, 1), 4)) == add(new, 4) .

which produces the output

reduce in QUEUE-OF-NAT : remove(add(add(new,1),4)) == add(new,4) 
rewrites: 7
result Bool: true