Real World Specs
Omer van Kloeten talks about Spec# in the Real World and points to Mike Barnett's talk about Spec# in the Lang.NET Symposium. While he likes the technology, he's worried that most developers will find it too inconvenient to use.
I am planning on adding specifications support including syntax highlighting on a minor update that will quickly follow the initial NStatic product. This is a minor addition, developmentwise, because, even in the initial product, specifications are automatically inferred for each method and class; you just can't enter them explicitly just yet except through use of asserts and throw clauses.
This points to a major difference in design goals between the Spec# guys and myself. I put a major focus on usability; in order to serve the most users, the product should be as frictionless and enjoyable to use as possible.
The Spec# and ESC/Java guys assume developers are "guilty until proven innocent" and require developers to explicitly make every assumption as Judah mentions. This code is suspicious; you must have committed a crime. This leads to extensive annotations baggage and a lot of work from developer such as this example in the Spec# mailing. Even with the effort required, Spec# misses this glaring hole from Judah's comment due to its modular design and lack of interprocedural analysis:
object foo = new object();
NStatic basically assumes that you are "innocent until proven guilty." Aha! I found the smoking gun; you did do it. The example above is trivially caught; the product also finds a class of redundancy errors that are missed by Spec#. All you need to do and open your project file and click the big "Scan" button.
The application proceeds quickly through the codebase, reporting errors as they are found, allowing the user to interactively correct errors as the scan is proceeding.
Background scanning and instant interactivity create a modal-free experience and eliminate the customary wait typical of most scanning and compilation tools. Even more, NStatic supports scanning of individual code files for more speed, even if the rest of the project doesn't compile.
New asserts, throw clauses and specifications can be added incrementally to a codebase over time.
Note: This is a prerelease product, so statement above is subject to change.