Spec#

Latest version: 1.0.20411
Added 2008-04-24

Programming system that is an attempt at a more cost effective way to develop and maintain high-quality software.

The Spec# system consists of:
- The Spec# programming language: an extension of 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 Visual Studio, 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. Codenamed Boogie, this tool 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.
Supports VS 2008 and 2005.

Built for .NET 2

Add-in

Free or free version available

Add to my favorites[NEW] What's this? Want to keep track of the latest versions of your favorite tools? Add tools to your favorites. This acts as a watch list. We'll email you when your favorite tools are updated. You can also visit your favorites page at any time to see what has been updated, or to remove tools from your list.

What's this? Want to keep track of the latest versions of your favorite tools? Add tools to your favorites. This acts as a watch list. We'll email you when your favorite tools are updated. You can also visit your favorites page at any time to see what has been updated, or to remove tools from your list.