Microsoft Research Projects of Interest – Contracts

Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.

Contracts

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. They act as checked documentation of external and internal APIs. The contracts in the form of a library are used to improve testing via runtime checking, enable static contract verification, and documentation generation. The use of a library has the advantage that all .NET languages can immediately take advantage of contracts (See another post on this). There is no need to write a special parser or compiler. Furthermore, the respective language compilers naturally check the contracts for well-formedness (type checking and name resolution) and produce a compiled form of the contracts as MSIL.

Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading. Spec# is a research vehicle that has been used to explore specifications and the dynamic/static tools that make use of them.

Dafny is an imperative object-based language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. It is designed to support the static verification of programs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers updatable ghost variables, recursive functions, and types like algebraic datatypes, sets, and sequences. Specifications and ghost constructs are used only during verification; the compiler omits them from the executable code. The Dafny verifier itself is run as part of the compiler and is powered by Boogie and Z3.

Abstract State Machine Language (AsmL) is an executable specification language which can also be used with XML and MS-Word for literate programming. AsmL models operate at the level of .Net assembly and therefore work with all .Net languages. AsmL is usable via Spec Explorer, a model-based testing tool. AsmL enables testing that a system behaves as intended before it is programmed by means of a model. A model program in AsmL works by looking at the relevant states of the actual program and finding where the two do not conform.