This post originated from an RSS feed registered with .NET Buzz by Dan Fernandez. Original Post: Spec# for Visual Studio .NET 2003 Feed Title: Dan Fernandez's Blog Feed URL: /msdnerror.htm?aspxerrorpath=/danielfe/Rss.aspx Feed Description: Dan discusses Dot Net. Latest .NET Buzz Posts Latest .NET Buzz Posts by Dan Fernandez Latest Posts From Dan Fernandez's Blog

From the research web site:

The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software.   The system consists of:

• A programming methodology, which includes a sound treatment of object invariants in object-oriented programs.
• The Spec# programming language, which is a superset of C# and adds things like non-null types, checked exceptions, method contracts (like pre- and postconditions), and object invariants.
• The Spec# compiler, which is integrated into the Microsoft Visual Studio development environment, statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the specifications in metadata for consumption by the program verifier.
• The Spec# static program verifier, which translates programs into logical verification conditions, which are passed to an automatic theorem prover.
• An interface to the SpecExplorer tool for test generation and model-based testing.

More info: http://research.microsoft.com/SpecSharp/

If you've ever read the Pragmatic Programmer or done contract-based programming before with tools like iContract, you'll instantly see the value of pre- and post- conditions for code.