Defensive programming, Design by Contract and Spec#
Fredrik Normén recently wrote an article about "Defensive programming and Design by Contract on a routine level" and I can't agree with him more. I'm a true believer in the defensive programming style he describes. Like Fredrik, I'm very interested in the development of Microsoft's Spec# language that's currently developed by Microsoft Research. Perhaps Spec# will RTM soon, but I actually doubt it.
I really like the idea of Spec#, but much more I'd like Spec# to be integrated in C# later on. C# is the preferred language in many software projects I work on and will be working on in the future. Convincing other programmers and management to use a more scientific language like Spec# will be hard.
The first Spec# feature that's on my C# list is the 'nullity discrimination' with the very intuitive T! syntax. A quote from the Spec# docs:
Many errors in modern programs manifest themselves as null-dereference errors, suggesting the importance of a programming language providing the ability to discriminate between expressions that may evaluate to null and those that are sure not to (for some experimental evidence, see [24, 22]). In fact, we would like to eradicate all null-dereference errors.
We have opted to add type support for nullity discrimination to Spec#, because we think types offer the easiest way for programmers to take advantage of nullity distinctions. Backward compatibility with C# dictates that a C# reference type T denote a possibly-null type in Spec# and that the corresponding non-null type get a new syntax, which in Spec# we have chosen to be T!. [->]
- .NET General, C# - No comments / No trackbacks - § ¶
