Home

Spec#

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.

By Ehud Lamm at 2005-05-04 12:31 | Software Engineering | other blogs | 21888 reads

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?

By Dominic Fox at Wed, 2005-05-04 14:52 | login or register to post comments

JML

For Java there's JML.

By Ronny Wichers Schreur at Wed, 2005-05-04 15:13 | login or register to post comments

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.

By raboof at Sat, 2005-05-07 10:08 | login or register to post comments

Rustan

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

By Ben Goetter at Sun, 2005-05-08 18:09 | login or register to post comments

Dbc for Java

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

By Ehud Lamm at Sat, 2005-05-07 15:29 | login or register to post comments

Design By Contract

Hi,

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

cu,
Bart

By deboeck at Mon, 2005-07-25 02:16 | login or register to post comments

ESC/Java

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.

By dcoetzee at Mon, 2005-07-25 18:11 | login or register to post comments