Spec#

Established: June 11, 2004

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 group.

  • People

    Many people worked on Spec#. Here is a partial list:

  • Download and Discussion Forum

    Spec# is available from the Spec# codeplex site in binary form as well as source form.

    The Spec# codeplex site also has a discussion forum, which is the best place to ask questions about Spec#.

  • Documentation

  • Project Members

    Other Contributors

     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#

  • Related Tools

    • 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

  • 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.

  • Publications

    • 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.

People

People

Portrait of Rob DeLine

Rob DeLine

Senior Principal Researcher