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.
of Programming Seminars