Fugue is a static
modular protocol checker developed
at Microsoft Research. Fugue, the
successor to Vault, can check any language that compiles to Microsoft's
Common
Language Runtime. Fugue provides the
programmer a set of annotations for specifying API usage rules.
For example, programmers can annotate
methods that allocate and release resources, or can specify a finite
state
machine for the order in which methods must be called. In this
talk, I will discuss the extensions
to Fugue that I implemented during my internship. These include
new annotations for specifying what exceptions a method
may throw, as well as the post-state of the target object when a method
throws
an exception. Fugue also now ensures
that resources are not leaked when exceptions are thrown. These
additions can be of great practical value: it is easy for
programmers to overlook
exceptional cases and difficult to uncover these errors during testing.
Principles
of Programming Seminars