Thursday, April 27, 2006


Spec# - Design By Contract for C#

Frank De prins reminded me about spec# from Microsoft Research, which extends the C# programming language to include contracts.

Preconditions ("requires") and postconditions ("ensures") will be familiar to Eiffelists, as will class invariants. Spec# also supports frame conditions ("modifies"), and explicit denotation of parts of code that may temporarily invalidate a class invariant ("expose").

There is also void-safety. Indeed, this might be the inspiration for the inclusion of void-safety in ECMA Eiffel, as Bertrand Meyer was closely involved with Microsoft's early work on the .NET platform.

Spec# checks contracts at runtime, and interfaces with the Simplify theorem prover for static verification.

Spec# integrates with VisualStudio, and can be downloaded for free.

A PDF document The Spec# Programming System: An Overview discusses contributions to systems with contracts (on pages 14-15). It mentions Gypsy, Alphard, Euclid and Clu as early influences, and lists Eiffel, SPARK and B as "modern systems with contracts that have had a direct effect on practical programs".

B isn't a programming language. It's at 100% a formal method with only logic, at the end of the process you can extract a programm from the model. But you can't say that is a programming language just for that.

Regard, Joris REHM
Oh sorry i have misunderstood : you haven't say that ... :)
I used to read the overview article looking for examples of function postconditions. C# does have "return" instead of Result, so omission may not be an accident.
Post a Comment

<< Home

This page is powered by Blogger. Isn't yours?