Experimental MicroSoft DotNet language - CsharpLanguage but with added functionality for DesignByContract.  From the website (modified to create WikiWords):

----
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 ObjectOriented language CsharpLanguage.  It extends the type system to include non-null types and CheckedException''''''s.  It provides method contracts in the form of pre- and PostCondition''''''s as well as ClassInvariant''''''s.
* The Spec# compiler.  Integrated into the Microsoft VisualStudio development environment for the DotNet 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.

see http://research.microsoft.com/specsharp/

CategoryProgrammingLanguage