|
|
Spec#
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.
There are two versions of Spec# available: one for Visual Studio 2005 and one for Visual Studio 2008.
Please follow the link for the version you have installed. If you are not using Visual Studio, then
it does not matter which one you download.
- Spec# for Microsoft Visual Studio .NET v1.0.20411 (11 April 2008)
Previous release notes:
1.0.11215 (15 December 2007),
1.0.10718 (18 July 2007),
1.0.7301 (1 May 2007),
1.0.7126,
1.0.6526,
1.0.6404,
1.0.6228,
1.0.6003,
1.0. 5920,
1.0.5818,
1.0.5626,
1.0.5612,
1.0.5424,
1.0.5301,
1.0.5030
We intend to update these releases regularly.
The Spec# installer does not require that you have Visual Studio installed.
(However, for academic users,
it is very inexpensive to be a part of the
Academic Advantage
program which provides licenses for all Microsoft operating system and developer tools
to faculty members and students.)
Vista users: If you see an error code of 2869 when you install Spec#, then you can try
disabling the user account controls by going to the Control Panel, then User Accounts, then
User Accounts (again), then Turn User Account Control on or off. Once you have installed Spec#,
you can re-enable the controls.
Note: There is no documentation in the distribution--as
documentation becomes available, it will be posted either here on this website
or on the Spec# Wiki.
We welcome bug reports, questions, feature requests, and, of course, praise; they can be sent to the
Spec# mailing list.
In this age of spam, we have had to restrict the list so only members can send email to it. The good news is that you can add yourself to the list
by sending the following
to the list.
-
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 20006 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.
-
The Spec#
Wiki is an open site for samples and documentation.
-
There is a new primer on how to write Spec# written by Rustan Leino!.
- 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 2005
Extends the Boogie methodology to concurrent programs.
- Iterators Revisited: Proof Rules and Implementation. [PDF]
Bart Jacobs, Erik Meijer, Frank Piessens, and Wolfram Schulte. In FTfJP 2005
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]
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 2004
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]
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.
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.
- 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
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
|
