Type and Behaviour Analysis

This system implements and visualises a Type and Behaviour Analysis for a non-trivial subset of CML; it is based on the theory developed in [1].

[1] Torben Amtoft & Flemming Nielson & Hanne Riis Nielson: Type and Effect Systems: Behaviours for Concurrency; to be published by Imperial College Press. Click here for an early version (DAIMI PB-529, October 1997).

Click here to start the analyser.

Input

A program written in the variant of CML described here. The main restriction compared to the full CML is that

the user cannot define constructors;
imperative features are not supported;
modules are not supported.

You can choose whether to enter the source program from a file or from keyboard.

Method

The default action of the system is to

translate the source program into an "equivalent" expression e belonging to a small subset of CML, called "NN-CML" (described here).
analyse this e, using (an extension of) algorithm W as described in [1], Chapter 4.

You can choose to suppress phase 2, if you want to see how your program is translated.

Output

If no parse/type error is reported, the system produces

an annotated type t
a behaviour b
a set of constraints C

such that

C,A |- e : t & b

([1], the Soundness Theorem 4.29), where |- is the typing judgement ([1], Fig. 2.8).

In addition, types and behaviours contain region information. Thus one can tell in which region a channel is allocated and in which region an input/output action is performed. A region is a set of labels, where a unique label is assigned to each syntactic channel construct.

Postprocessing

After the main part of the analysis has finished, producing t, b, and C, the result can be examined, post-processed, and subsequently displayed, in various ways:

You can take a look at t, b, and (the "raw constraints") C. Warning: For all but very small programs this will probably be quite unreadable, due to the large number of constraints.
You can get an "interpretation" of t, an interpretation of b, together with an interpretation of the (behaviour) variables mentioned there. This will in general produce quite readable information. (The behaviour "..." denotes a possibly non-terminating "sequential" computation.)
Alternatively, you can restrict your attention to selected regions. This will probably result in very concise information, with the following classification of computations which do not spawn any processes and which only affect (allocate, read, write) "hidden" (non-selected) regions:
- "tau_n" denotes a terminating computation, with at most n "concurrent" actions taking place;
- "rec_n" denotes a possibly non-terminating computation, with at most n "concurrent" actions taking place;
- "rec_oo" denotes a computation which may have an unbounded number of "concurrent" actions.
Alternatively, you can choose to let "..." denote either of these three.
You can click on the name of a let-bound identifier, in order to see the type scheme assigned to it.

The system is experimental; please send comments to tamtoft@daimi.au.dk.

Click here for a system working directly on NN-CML programs.

The system is implemented in Moscow ML by Torben Amtoft; the parsing of CML and the translation into NN-CML was originally written by Kirsten L. S. Gasser.

The interface is heavily inspired by the system for Control Flow Analysis, implemented by Kirsten L. S. Gasser, Sharmila R. Lassen and Hanne Riis Nielson, which borrows ideas from Peter Sestoft.