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.
The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. Spec# is pronounced “Spec sharp” and can be written (and searched for) as the “specsharp” or “Spec# programming system”. The Spec# system consists of:
- The Spec# programming language. Spec# is an extension of the object-oriented language C#. It extends the type system to include non-null types and checked exceptions. It provides method contracts in the form of pre- and postconditions as well as object invariants.
- The Spec# compiler. Integrated into the Microsoft Visual Studio development environment for the .NET platform, the compiler statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools.
- The Spec# static program verifier. This component (codenamed Boogie) generates logical verification conditions from a Spec# program. Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it.
A unique feature of the Spec# programming system is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads, and inter-object relationships.
The Spec# programming system is being developed as a research project at Microsoft Research in Redmond, primarily by the Programming Languages and Methods group.
- The best place to learn about Spec# is the Spec# tutorial.
- Slides from a recent Spec# tutorial workshop by Rosemary Monahan and Rustan Leino are available from here.
- Arnd Poetzsch-Heffter has a great set of slides from a course he taught at Winter School 2009.
- Program Verification Using the Spec# Programming System. (Tutorial presented at ETAPS 208 by Rustan Leino and Rosemary Monahan.) [ppt]
- Towards a Verifying Compiler: The Spec# Approach: Lecture 1, Lecture 2, Lecture 3, Lecture 4, Lecture 5. (A tutorial presented at Marktoberdorf 2006 and FM 2006).
- Spec#: Adding Contracts to C#. A free MSDN webcast available on-demand. It was presented live on 4 May 2005.
- The Spec# Programming System: An Overview. Slides of a tutorial presented at FM 2005 in Newcastle, UK.
- Mike Barnett
- Manuel Fähndrich
- Rustan Leino
- Francesco Logozzo
- Peter Müller
- Wolfram Schulte
- Herman Venter
- Songtao Xia
- Rob DeLine, Microsoft Research
- Rosemary Monahan, NUI Maynooth
- Madan Musuvathi, Microsoft Research
- Dave Naumann, Stevens Institute of Technology
- Frank Piessens, Katholieke Universiteit Leuven
- Burkhart Wolff, University Paris-Sud
Past Summer Interns
- Evan Chang, UC Berkeley, 2004, 2005
- Adam Darvas, ETH Zurich, 2006
- Diego Garbervetsky, Universidad De Buenos Aires , 2006, 2007
- Bart Jacobs, Katholieke Universiteit Leuven, 2005
- Ronald Middelkoop, TU Eindhoven, 2007
- Simon Ou, Princeton, 2004
- Ralf Sasse, University of Illinois at Urbana-Champaign, 2007
- River Sun, Stevens Institute of Technology, 2004
- Angela Wallenburg, Chalmers University of Technology and Göteborg University, 2006
See What Others Are Saying about Spec#
- Greg Young’s I want Spec# page.
- A Hanselminutes podcast interview that Rustan Leino and Mike Barnett did with Scott Hanselman.
- A video Greg Young took of a Spec# presentation at altdotnet on 19 April 2008.
- Computerworld, an interview with Rick Rashid, Senior Vice President, Microsoft Research
- Dr. Dobb’s Portal
- Microsoft Research News & Highlights
- .NET Rocks, an Internet Audio Talk Show interview with Rustan Leino
- Smart Software
- Lambda the Ultimate
- C# Chat in MSDN (Just a question about it; search in the page for “Spec#”.)
- Code Contracts. (Soon to be on DevLabs and part of .NET 4.0!) This includes Clousot, the abstract-interpretation based static analysis tool.
- Pex, the amazing unit-testing tool. (Available on DevLabs!)
- The SpecExplorer tool for test generation and model-based testing uses a version of Spec# for its input. (But note, to use SpecExplorer, you must use its own compiler.)
- Java Modeling Language (JML), which supports a variety of checking tools.
- The Splint annotation-assisted lightweight static checker for C programs
We provide some benchmarks that can be used to compare the power and performance of other program verifiers and theorem provers. These are generated from the Boogie test suite, and consist of BoogiePL programs (the majority of which were produced by Boogie from Spec# programs in the Boogie test suite) and the verification conditions that Boogie produced from these BoogiePL programs in the format of the Simplify theorem prover.
- Boogie benchmarks, 6 Oct 2006 [9 MB compressed zip file]
- The Spec# programming system: An overview. [PDF]Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. In CASSIS 2004, LNCS vol. 3362, Springer, 2004.Describes the vision and architecture of the Spec# programming system.
- Boogie: A Modular Reusable Verifier for Object-Oriented Programs. [PDF]Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. In FMCO 2005, LNCS vol. 4111, Springer, 2006.Describes the architecture of the Boogie program verifier.
- Verification of object-oriented programs with invariants. [Electronic version]Mike Barnett, Rob DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte. JOT 3(6), 2004.Gives a formal account of the programming methodology in Spec# (which has been referred to as the “Boogie methodology”).
- Exception safety in C#. [PDF]K. Rustan M. Leino and Wolfram Schulte. In SEFM 2004, IEEE, 2004.Describes the design rationale for exception handling in Spec# and why it differs from C#.
- Abstract Interpretation with Alien Expressions and Heap Structures. [PDF]Bor-Yuh Evan Chang and K. Rustan M. Leino. In VMCAI 2005, LNCS vol. 3385, Springer, 2005.Describes the architecture (used in Boogie’s abstract-interpretation engine for inferring invariants) of combining abstract domains via an equivalence graph and applies a particular abstract domain that handles values in the object heap.
- Inferring object invariants. [PDF]Bor-Yuh Evan Chang and K. Rustan M. Leino. In AIOOL, 2005.In the context of the Boogie methodology, describes how to infer object invariants from the source code.
- Modular verification of static class invariants. [PDF]K. Rustan M. Leino and Peter M�ller. In FM 2005, to appear.Presents a specification and verification methodology for dealing with class-level invariants, including static fields.
- Safe Concurrency for Aggregate Objects with Invariants. [PDF]Bart Jacobs, K. Rustan M. Leino, Frank Piessens, and Wolfram Schulte. In SEFM 2005Extends the Boogie methodology to concurrent programs.
- Iterators Revisited: Proof Rules and Implementation. [PDF]Bart Jacobs, Erik Meijer, Frank Piessens, and Wolfram Schulte. In FTfJP 2005Proposes a specification and verification method for iterators and foreach loops. Also, describes nested iterators, which allow efficient traversal of recursive data structures.
- Object invariants in dynamic contexts. [PDF]K. Rustan M. Leino and Peter Müller. In ECOOP 2004, LNCS vol. 3086, Springer, 2004.Extends the Boogie methodology with visibility-based invariants.
- 99.44% pure: Useful Abstractions in Specifications. [PDF]Mike Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun. In FTfJP 2004A method for allowing methods that have restricted side-effects to be used in specifications.
- Friends Need a Bit More: Maintaining Invariants Over Shared State. [PDF]Mike Barnett and David A. Naumann. In MPC 2004.A methodology for relaxing the ownership system in Spec#.
- Towards Imperative Modules: Reasoning about Invariants and sharing of mutable state. [PDF]David A. Naumann and Mike Barnett. In LICS 2004.The theory underlying the Friends methodology which encompasses the Spec# ownership system.
Senior Principal Researcher