Lambda the Ultimate

inactiveTopic Fugue: A Protocol Checker for the dotNET CLR
started 6/3/2003; 12:06:58 PM - last post 6/3/2003; 12:06:58 PM
Ken Hirsch - Fugue: A Protocol Checker for the dotNET CLR  blueArrow
6/3/2003; 12:06:58 PM (reads: 242, responses: 0)
From Manuel A. Fähndrich and Rob Deline, the people who brought you Vault, comes Fugue, a "protocol checker" that brings many of the ideas from Vault to .NET.

The Fugue protocol checker: Is your software Baroque?

Fugue analyzes code in any language that compiles to the Common Language Runtime (CLR) ,such as C, Visual Basic.NET and Managed C++. While a modular analysis does require extra specifications,the benefit is that the analysis can be performed fast enough to be run after every compilation.
...
Fugue builds on our previous work on the Vault programmming language, which in turn is based on type-state checking and the Capability Calculus. ... Fugue’s main innovations over Vault are state mapping, custom states, and plug-in pre- and postconditions, for which Vault has no equivalents.
They use the "plug-in pre- and post-conditions" to validate SQL statements at compile-time. Pretty neat.

Fugue is briefly compared with other related work: SLAM, ESP, ESC, Metal, and Prefix.

An interesting quote: "However, having the programmer annotate every object’s lifetime as part of its type proved to be a considerable burden."

Links:

Microsoft Research

Other: