|
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.
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:
|
Fugue: A Protocol Checker for the dotNET CLR