Donna Malayeri

Carnegie Mellon University

Specifying and Checking Exception Effects in Fugue


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

Friday, September 26, 2003
3:30 p.m.
Wean Hall 8220