Corejava is part of the CZT project that aims at providing a framework for building formal methods tools, especially for the Z specification language. This subproject provides AST (Annotated Syntax Tree) classes for Z written in Java.

If you are a Z user and you are looking for existing Z tools, you might be more interested in other, more user oriented subprojects of CZT (which often use the classes provided here). If you are a developer of Z tools, this might be exactly what you are looking for.

Features are:

Visitor Support in Corejava

Corejava provides a variant of the default visitor introduced by Martin E. Nordberg III. The default visitor adds another level of inheritance to the visitor pattern. It provides the possibility to implement default behaviour by taking advantage of the inheritance relationship of the classes to be visited. Nordberg achieves this by deriving the default visitor from the standard visitor, adding visit methods for each abstract AST class, and implementing the visit methods in such a way that the visit method for a class Foo calls the visit method for class Bar where Bar is the base class of Foo. The CZT AST classes already support visit methods for abstact classes. Each AST class Foo, concrete as well as abstract, has a corresponding FooVisitor interface defining the visitFoo method. A visitor may or may not implement this particular interface. If an instance of class Foo accepts a visitor, it checks whether the visiting visitor implements FooVisitor. If this is the case, this method is called. However, if the accepted visitor does not implement FooVisitor, it is checked whether it implements BarVisitor where Bar is the base class of Foo, etc. This way, the AST classes itself take care of calling the closest (with respect to inheritence hierachy) visit method implemented by the visitor.

This makes it very easy to implement a visitor that visits each element of an AST without being forced to implement all visit methods for concrete classes: 

public SimpleVisitor implements TermVisitor
{
  public Object visitTerm(Term term)
  {
    Object[] args = term.getChildren();
    for (int i = 0; i < args.length; i++) {
      if (args[i] instanceof Term) {
        ((Term) args[i]).accept(this);
      }
      else if (args[i] instanceof List) {
        // handle lists ...
      }
    }
    return null;
  }
}