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".
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".
posted by Roger Browne @ 17:47 
Comments:
<< Home
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
Regard, Joris REHM
# posted by 
: 27 April, 2006 21:29
: 27 April, 2006 21:29
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
# posted by : 02 May, 2006 12:29
: 02 May, 2006 12:29 << Home
