Mool

The Language

Mool is a mini object-oriented language in a Java-like style with support for concurrency, that allows programmers to specify class usage protocols as types. The specification formalizes (1) the available methods, (2) the tests clients must perform on the values returned by methods, and (3) the existence of aliasing and concurrency restrictions, all of which depend on the object’s state.

Linear and shared objects are handled as a single category, allowing linear objects to evolve into shared ones. The Mool type system verifies that methods are called only when available, and by a single client if so specified in the usage type. Mool builds upon previous works on (Modular) Session Types and Linear Type Systems.

Some Examples

The language main programming features and concepts are best described by some examples. You can download the complete set of examples in the Examples section.

The Petition

An online petition service starts with the submission of the title of the petition ("Save the Iberian wolf" in the example), and the deadline for signature collection. Then, time comes for promoting the petition: signing and disseminating. The petition writer signs the petition, and must get others to sign it. Hopefully the writer’s acquaintances will further sign and disseminate the petition, thus contributing to the success of the campaign.

Class PetitionServer has one single purpose: to create Petition references. Class Petition implements the (linear) protocol for submitting and the (unrestricted) one for promoting the petition. Class Signatory is on the client side, as well as class SaveTheWolf, which conducts the petition setup.

The FileReader

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. Class FileReader does exactly that by implementing the File protocol formally described in the class usage type. The FileReader, in turn, exposes in its own file reading protocol, additionally offering a choice of obtaining the file contents read up to a given point, and eventually providing unrestricted multi-threaded access to the file contents.

The Auction

Sellers want to sell items for a minimum price. Bidders place bids in order to buy some item for the best possible price. The auctioneer controls these interactions. The distinguishing feature in this example is the specification of the (linear) protocols in the form of two classes - the Selling and the Bidding - which the Seller and Bidder classes implement. Class Auctioneer creates the Auction instances, which are saved in the AuctionMap, and returns Selling and Bidding references to the several Seller and Bidder clients.


Team:

  • Joana Campos
  • Vasco Vasconcelos
  • Project:

    ASSERTION-TYPES for Object-Oriented Programming

    URL:

    http://gloss.di.fc.ul.pt/mool