Mool

MOOL, a mini Java-like object-oriented language that allows programmers to specify class usage protocols as types. The formalization specifies (1) the available methods, (2) the tests clients must perform on the values returned by methods, and (3) the existence of aliasing restrictions, all of which depend on the object's state. Additionally, the language includes a simple concurrency mechanism for thread spawning.

Motivation

There are several reasons why a type system should enforce that an object, and its methods, should only be available under specific conditions. For example, reading from a file should follow the rules of a well-known usage protocol: first a file must be opened, then it can be read multiple times (without reading beyond the end-of-file), and finally it must be closed. Additionally, read and close are intended to be operations over a linear object.

Usage protocols are typically described in informal documentation that cannot be verified by the compiler. Mool, however, incorporates usage protocols into types (which can be statically verified). Unlike other approaches, Mool does not use method annotations; instead, Mool allows you to attach a usage specification at the class level to define how class instances should be used. Linear and unrestricted annotations can further be used to describe the object status at any given moment. Mool lets linear objects evolve into shared ones.

Usage Types

Let's start with some less obvious syntactic details. Suppose a program defines a conventional class named C with methods m1, m2 and m3.

If C is intended to be used in an unrestricted fashion (instances of this class can be freely shared), and no usage is declared, Mool's compiler inserts a default (recursive) branch type of the form:

    usage *{m1 + m2 + m3}

A choice between calling one of the three available methods is indicated by (+). The un qualifier is omitted in unrestricted types. Calling any of these methods on an instance of C will not change the object state nor the set of available methods (just like a regular Java class).

If C is intended to be used linearly, a possible usage declaration might be:

    usage lin{m1; lin{m2; lin{m3; end;}}};

Calling methods in the prescribed order on an instance of C changes the object state and the set of available methods. Note that end is an abbreviation for un{}.

If the result of calling m2 is a boolean whose value that determines the next state, then a possible usage declaration might be:

    usage lin{m1; NextState} where
        NextState = lin{m2; <lin{m3; end;} + end>};

We call <lin{m3; end;} + end> a variant type. If m2 returns true, then after C[lin{m1; NextState}] the next state will be C[lin{m3;end;}]; otherwise it will be C[end], where end indicates there are no available methods. NextState is a symbolic name representing the full type lin{m2; <lin{m3; end;} + end>}.

A File Protocol

The File class usage type, whose behaviour has been informally described to motivate Mool, can now be specified as follows:

class File { 
    usage lin{open; Read} where 
    Read = lin{eof; <lin{close; end} + lin{read; Read}>};
  ...
}

A FileReader uses an object of class File, and supports multi-threaded access once the contents of the file has been obtained. It hides the File protocol from clients, revealing its own. We specify it like this:

class FileReader {
    usage lin{open; Next} where 
    Next = lin{next; <Next + Done> + toString; Next}
    Done = *{toString + getCounter};
  ...
}

Comparing the two usages, we note that an object of class File is linear from beginning to end, while an object of class FileReader starts linear, but then evolves into state Done where the specified methods may be called by multiple threads. Here's how we implement methods open and next on class FileReader (note that the code reveals a perfectly natural implementation of a file reader):

class FileReader {
   ...
   unit open() {
     f = new File(); // f is a field 
     f.open(); 
     s = ""; 
     // To track the number of accesses 
     counter = 0;
  }

  boolean next() {
    if(f.eof()) {
      // The file can be closed 
      f.close(); 
      false; // return false
    } else {
      s = s ++ f.read(); 
      true; // return true
    }
  }
  ...
}

After opening the file in method open, field f changes its type to File[Read], where the next available method is eof that returns a result of type boolean on which depends the object subsequent state. A test must performed in order to find out whether the end-of-file has been reached, and the file must be closed by calling method close on f.

To run the File Protocol classes, as well as other more extensive examples, please go to the Examples section.

Limitations & Bugs

Mool is a prototype, and there are some known limitations and probably some bugs. We are gradually working on identifying and fixing our tool.

Run
$