Spec# - Microsoft Research (original) (raw)

• Publications

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.

• Overview

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 (opens in new tab) group.

• Documentation

  • The best place to learn about Spec# is the Spec# tutorial (opens in new tab).
  • Slides from a recent Spec# tutorial workshop by Rosemary Monahan and Rustan Leino are available from here (opens in new tab).
  • Arnd Poetzsch-Heffter has a great set of slides (opens in new tab) from a course he taught at Winter School 2009 (opens in new tab).
  • Program Verification Using the Spec# Programming System. (Tutorial presented at ETAPS 208 by Rustan Leino and Rosemary Monahan.) [ppt (opens in new tab)]
  • Towards a Verifying Compiler: The Spec# Approach: Lecture 1 (opens in new tab), Lecture 2 (opens in new tab), Lecture 3 (opens in new tab), Lecture 4 (opens in new tab), Lecture 5 (opens in new tab). (A tutorial presented at Marktoberdorf 2006 and FM 2006).
  • Spec#: Adding Contracts to C# (opens in new tab). A free MSDN webcast available on-demand. It was presented live on 4 May 2005.
  • The Spec# Programming System: An Overview (opens in new tab). Slides of a tutorial presented at FM 2005 in Newcastle, UK.

• Project Members

  • Mike Barnett (opens in new tab)
  • Manuel Fähndrich
  • Rustan Leino (opens in new tab)
  • Francesco Logozzo
  • Peter Müller (opens in new tab)
  • Wolfram Schulte
  • Herman Venter
  • Songtao Xia

Other Contributors

• Rob DeLine (opens in new tab), Microsoft Research
• Rosemary Monahan (opens in new tab), NUI Maynooth
• Madan Musuvathi (opens in new tab), Microsoft Research
• Dave Naumann (opens in new tab), Stevens Institute of Technology
• Frank Piessens (opens in new tab), Katholieke Universiteit Leuven
• Burkhart Wolff (opens in new tab), University Paris-Sud

Past Summer Interns

• Evan Chang (opens in new tab), UC Berkeley, 2004, 2005
• Adam Darvas (opens in new tab), ETH Zurich, 2006
• Diego Garbervetsky (opens in new tab), Universidad De Buenos Aires , 2006, 2007
• Bart Jacobs (opens in new tab), Katholieke Universiteit Leuven, 2005
• Ronald Middelkoop, TU Eindhoven, 2007
• Simon Ou (opens in new tab), Princeton, 2004
• Ralf Sasse (opens in new tab), University of Illinois at Urbana-Champaign, 2007
• River Sun, Stevens Institute of Technology, 2004
• Angela Wallenburg (opens in new tab), Chalmers University of Technology and Göteborg University, 2006

• See What Others Are Saying about Spec#

  • Greg Young’s I want Spec# (opens in new tab) page.
  • A Hanselminutes podcast (opens in new tab) interview that Rustan Leino and Mike Barnett did with Scott Hanselman (opens in new tab).
  • A video (opens in new tab) Greg Young (opens in new tab) took of a Spec# presentation at altdotnet (opens in new tab) on 19 April 2008.
  • Computerworld (opens in new tab), an interview with Rick Rashid, Senior Vice President, Microsoft Research
  • Dr. Dobb’s Portal (opens in new tab)
  • Microsoft Research News & Highlights
  • .NET Rocks (opens in new tab), an Internet Audio Talk Show interview with Rustan Leino
  • Smart Software (opens in new tab)
  • Lambda the Ultimate (opens in new tab)
  • C# Chat in MSDN (opens in new tab) (Just a question about it; search in the page for “Spec#”.)

• Related Tools

  • Code Contracts (opens in new tab). (Soon to be on DevLabs (opens in new tab) and part of .NET 4.0!) This includes Clousot, the abstract-interpretation based static analysis tool.
  • Pex (opens in new tab), the amazing unit-testing tool. (Available on DevLabs (opens in new tab)!)
  • The SpecExplorer (opens in new tab) 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 (opens in new tab)), which supports a variety of checking tools.
  • The Splint (opens in new tab) annotation-assisted lightweight static checker for C programs

• Benchmarks

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 (opens in new tab), 6 Oct 2006 [9 MB compressed zip file]

• Publications

  • The Spec# programming system: An overview. [PDF (opens in new tab)]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 (opens in new tab)]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 (opens in new tab)]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 (opens in new tab)]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 (opens in new tab)]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 (opens in new tab)]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 (opens in new tab)]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 (opens in new tab)]Bart Jacobs, K. Rustan M. Leino, Frank Piessens, and Wolfram Schulte. In SEFM 2005_Extends the Boogie methodology to concurrent programs._
  • Iterators Revisited: Proof Rules and Implementation. [PDF (opens in new tab)]Bart Jacobs, Erik Meijer, Frank Piessens, and Wolfram Schulte. In FTfJP 2005 (opens in new tab)Proposes 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 (opens in new tab)]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 (opens in new tab)]Mike Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun. In FTfJP 2004 (opens in new tab)A 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 (opens in new tab)]Mike Barnett and David A. Naumann. In MPC 2004 (opens in new tab).A methodology for relaxing the ownership system in Spec#.
  • Towards Imperative Modules: Reasoning about Invariants and sharing of mutable state. [PDF (opens in new tab)]David A. Naumann and Mike Barnett. In LICS 2004 (opens in new tab).The theory underlying the Friends methodology which encompasses the Spec# ownership system.

People

Rob DeLine

Senior Principal Researcher