Katja Example: Invoices

This example demonstrates the following Katja features:

  • Types are generated immutable.
  • Supports the use of the basic Java types and Strings.
  • Supports definition of tuples and lists.
  • Creates convenient methods for construction and selection of terms.
  • Creates convenient methods to change tuple components.
  • Creates interfaces and support methods to visit terms.

Specification

A Katja specification for invoices simply starts like this:

specification Invoices

Every specification has a name, which is used as a name for the factory class.

backend java {
  package Billing
  import java.lang.String
  import java.lang.Integer as Int
}

Katja supports other languages than Java, so this is why Java specific settings are defined in a so called backend block. What we define here is in which Java package the generated types reside in and which Java types we like to use in the specification. We can also relabel those types as we like.

Now we start with actually defining data types:

external String
external Int

These types are declared to just exist, Katja does not know anything about them. We defined their meaning in the backend block.

Please note that the lines up to this point are standard for most specifications and can in fact be used as a template. The essence of a specification is what follows now; the definition of tuples, lists, etc.

Invoice ( String customerID, Int total, Item* items )
Item ( String name, Int amount )

We define Invoice to be a tuple with three components. A String called customerID, an Integer called total and a list of Items called items. An Item is also a tuple, in specific a pair of name and amount. We have also defined ItemList with an abbreviated syntax. Normally we would have to write ItemList * Item (in a separate line) to define ItemList to be a list of items (we could also have called it Items to be shorter).

The listing for this example is can be stored in an arbitrary named file, in this example we use inv.katja.

To compile it into a library using the Katja compiler, we can use the following invocation:

sh katja-jar -b java -o -j inv.katja

It invokes Katja from the library file katja.jar, using the shell script katja-jar. The -b option selects the Java backend, -o (override) tells Katja it is ok to replace en existing library and -j deploys a jar file called katja.common.jar, which is needed by every generated library Katja will produce. The last parameter, of course, is the specification file. Katja will now generate a library contained in a jar file named like the specification, i.e. Invoices.jar in our case.

If you want to try the example, but do not want to compile the specification yourself, you can download the library Invoices.jar and the common library katja.common.jar.

Sample Java Code

A sample Java file working with the generated library could look like this:

The first thing you most often want to do is import all the factory methods to construct terms and then import all the types you have specified in your specification:

import static Billing.Invoices.*;
import Billing.*;

public class Test {
    public static void main(String... args) {

These lines create a new Invoice using the static factory methods from the specification class Billing.Invoices. Note that autoboxing is indeed a nice feature of Java 5:

        Invoice inv =
            Invoice("07743196", 0,
                Item("One of these", 17),
                Item("One of those", 11)
            );

We now want to calculate and change the total of the invoice, using a method written by someone else. Note that we pass the complete Invoice to the method, yet we do not want the callee to change it! We are only interested in the integer result:

        inv = inv.replaceTotal(calculateTotal(inv));

Finally we want to pretty-print our Invoice:

        new InvoicePrinter().visit(inv);
    }

The calculateTotal method is very easy to implement:

    public static int calculateTotal(Invoice inv) {
        int total = 0;

        for (Item i : inv.items()) total += i.amount();

        // malicious - but useless - attempt to remove all items
        inv.replaceItems(ItemList());

        return total;
    }
}

As all data types are created immutable, the attempt to change the invoice is in vain. The method just creates a local, modified version the Invoice, like it is with Strings. The result, however, is immediately discarded by the method.

We implement the InvoicePrinter using a visitor, which is supported by Katja:

class InvoicePrinter extends Invoice.Visitor {

    public void visit(Invoice inv) {
        System.out.println("INVOICE for customer " + inv.customerID());
        visit(inv.items());
        System.out.println("  Total: " + inv.total());
    }

    public void visit(ItemList list) {
        for(Item i : list) visit(i);
    }

    public void visit(Item i) {
        System.out.println("  - " + i.name() + ": " + i.amount());
    }

    public void visit(Integer n) {}
    public void visit(String s) {}
}

The listing of this test file is Test.java, according to Java conventions.

To compile the file, we can use the following invocation of javac:

javac -cp Invoices.jar:katja.common.jar Test.java

All we have to make sure is that we have the generated library, as well as the common library in the classpath. The same is true for starting the Test program:

java -cp Invoices.jar:.:katja.common.jar Test

As expected, we will get the correct result:

INVOICE for customer 07743196
  - One of these: 17
  - One of those: 11
  Total: 28

Files of the Example

All links in one place:

Version

The example and attached files are updated for version 5824 (most notably the =visit= methods).