Spec# is 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# static program verifier. This component translates Spec# programs into logical verification conditions. Internally it uses an automatic theorem prover that operates on the verification conditions deduced from the Spec# contract. An interface to the Spec Explorer tool for test generation and model-based testing.

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.

Spec# (also "specsharp" for search engines and the like), is now available for download. The home page gives a list of related publications.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Good stuff

This is a pretty neat integration of DBC into C#, pretty immediately accessible for current C# coders. I could see myself starting to add invariants and pre-/post- conditions into my code tomorrow; and I could see them making that code considerably more robust (and better documented).

There must surely be similar things for Java already?


For Java there's JML.

K. Rustan M. Leino

Interestingly, one of the main characters in the original development of the ESC/Java tool (the `Extended Static Checker' for Java), K. Rustan M. Leino, is now involved in Spec#.

A very exciting and promising field, if you ask me.


He's a character, all right....

Dbc for Java

There are plenty of DbC tools for Java (e.g., jContract, iContract etc.).

Design By Contract


A blog about SpecSharp : http://www.xenopz.com/blog/bartdeboeck/CategoryView,category,Design%20by%20contract.aspx



Actually, the closest technology to Spec# for Java by a long shot is ESC/Java, which is based on very similar ideas, except that it doesn't feature object invariants and some other new features of Spec#. In fact, some of the same people worked on both projects.