A prototype static analysis tool for observable effects

I've had a piece of code kicking around for a while that hasn't really been doing anything, so I've decided to wrap it in a basic web front-end and unleash it upon the unsuspecting public.

It's a tool for performing a very basic kind of specification checking for a simple ML-like language. The idea is that you construct a specification consisting of *traces* of observable effects, and then the compiler can statically determine whether your program behaves according to this specification. It does this by automatically inferring a process algebra-like behavioural type for the program, and then using this as a representation against which to perform specification checking in a tractable way.

An example:

OPERATIONS
insertCoin
button1
button2
takeDrink1
takeDrink2
coinReturnButton
takeCoin

NECESSARY

SAFE
insertCoin,button1,takeDrink1
insertCoin,button2,takeDrink2

FORBIDDEN
insertCoin,_*,insertCoin

The Operations section defines which operations are of interest to us. Naturally our program could be producing any number of observable actions, but we may only be interested in specifying certain types of behaviours. In this case, we're specifying a program that interacts with a vending machine.

Each action (e.g. insertCoin) corresponds to some library call in the language that produces a side-effect. Because the language (which I will describe shortly) is "mostly functional" (in the style of ML), there is no mechanism to introduce new side-effects - they have to come from a built-in library function, or some foreign function interface.

The (empty) Necessary section is the strongest type of specification - it says "the program must be able to behave according to all of these traces, and must not be able to exhibit any other behaviour". When it is empty (as in this example), it has no effect.

The Safe section specifies a weak liveness property, "the program must be able to behave according to at least one of these traces". We have two separate traces defined in our Safe section in this example, each corresponding to a "sensible" interaction between our program and the vending machine. The compiler will halt and issue an error if the program is not able to behave according to any of the traces in a non-empty Safe section.

The final section is the Forbidden traces. These act as a general "pattern match" across all the possible behaviours that a program is able to exhibit. In this case, we specify that we never want our program to be able to insert two coins into the machine. The underscore (_) operator is a wild card, standing for any action that appears in the Operations section. The asterix (*) has the normal meaning one would expect from regular expressions, meaning "zero or more occurrences of this action". So the final trace demands that there never be two occurrences of insertCoin in any of the possible program behaviours.

Now, an implementation!

fun main x = let v = insertCoin () in (if rand_boolean() then ((button1 ());(takeDrink1 ())) else ((button2 ());(takeDrink2 ())))

val _ = main ()

Now this implements our specification. The web-based tool will report "specification satisfied", and will print a visual representation of the behavioural type that it has inferred from the program text.

The tool is at: http://www.expdev.net/tracespec/

I will upload the (as of yet) unpublished paper describing the internals of the system and hopefully some better examples and documentation later tonight. Let me know if you would like to know more.

The tool is pretty fragile at the moment. The error reporting is very bad in most cases. Let me know if you come across any totally weird behaviour, because part of this unleashing-on-the-public exercise is to try to figure out what is and isn't working, and how I can improve it, so I would appreciate any feedback.

The idea (before you ask) is the encourage a very light weight form of specification. There is no execution going on here. It is supposed to mimic the function of certain types of unit tests in a completely static way. The way it is implemented at the moment is a rough prototype. Once I have proved to myself that this is a feasible kind of static analysis to perform, I may work on integrating it into a compiler for a general-purpose language. There is no particular restriction on the source language, however it is most likely to be feasible for a strongly typed functional language.

• The tool: http://www.expdev.net/tracespec
• An (unpublished) paper describing the system: http://www.expdev.net/tracespec/doc/tracespec.pdf - A few things have changed, as I have been developing the system further to overcome the limitations described in the paper.
• A few small examples: http://www.expdev.net/tracespec/doc/examples/
• A Git repository and source code will follow shortly. In the mean time, you can contact me by adding gian.perrone to @ and gmail.com in order to get an email address.