TRIM is an abstract machine capable of executing a subset of the algebraic specification language OBJ3. The subset of OBJ3 was chosen in such a way that it reflects all the semantic components of the language but omits some of the syntactic constructs present in the current version of OBJ3. A specifically designed compiler translates the order sorted conditional equations of an OBJ3 specification into the abstract term rewriting machine code -- the TRIM code.

To obtain more efficient target code we include two optimizers in our compiler system; a peep-hole optimizer and a rule-base optimizer. Peep-hole optimizers improve the efficiency of programs by successively applying behavior preserving optimization rules to the original program. The rule-base optimizer prevents unnecessary attempts of equation application to an input term for which one knows the application will fail. It accomplishes this by splitting the set of equations in an OBJ3 specification into partitions such that, if one equation application in a particular partition fails, then none of the other equations in the same partition are tried.

The compiler, optimizer, and the abstract term rewriting machine have been seamlessly integrated into the OBJ3 environment. The implementation in C++ comprises about 15,000 lines of code. The system provides a speedup of about one order of magnitude over the interpreted OBJ3 equations.

For a more detailed discussion of TRIM please refer to the document Introducing TRIM. The integrated OBJ3/TRIM system can be downloaded from http://www.kindsoftware.com.

Example: Consider the rewrite rule

               (var X:Int) eq X * 1 = X .

                         ...

                        MATCH * 2 ;
                        JUMPF L5 ;
                        BIND X [ Int ] ;
                        JUMPF L5 ;
                        MATCH 1 0 ;
                        JUMPF L5 ;
                        KILLOP ;
                        GET X ;
                        APPLY ;
        L5 :
                         ...

The generated code attempts to match the input term by doing a prefix, depth-first traversal of the left-hand side term of the given rewrite rule. In this case, it attempts to first match the * operator to the input term, then it tries to bind the variable X observing its sort Int, and lastly it attempts to match the constant operator 1. Should a match or binding fail, then control is passed to the code following the rule with the JUMPF instruction (short for "jump if false"). Once the input term is matched it is removed with the KILLOP instruction and the replacement term is computed. Here this is simply a retrieval of the term bound to the variable X. Finally, the replacement term is inserted into the input term via the APPLY instruction.