Is Spec# stable enough to use? [closed]

Question

Does anyone here use Spec# regularly? I would like to know if it is stable and powerful enough before I start using it everywhere. It looks like the syntax is influencing c# 4.0, which will hopefully make it easier to upgrade once 4.0 is released. Thoughts?

Empirin

Use everywhere? Only if it's documented you should take that route. Clearly it's not the case, which signals it's an experimental/research-oriented in-house product. Spec#, Sing#, C-omega, F* there are quite a few like this. On the other hand to try something out Nemerle or Boo will be better alternatives. – Scriabin

Answer 1

I guess it depends on what you mean by "stable". There are two possible interpretations:

1. "not crashing"
2. "not changing"

I don't know about #1, but if you mean #2, then, well, Spec# has been abandoned and is no longer being developed, so that's probably as stable as you're gonna get.

The techniques and tools that were used in Spec# (the static analysis tool called Boogie and the theorem prover / constraint solver Z3) are now part of a new library called Code Contracts for .NET. The upshot of being a library is that Code Contracts will work for any .NET language: C#, VB.NET, F#, Ruby, Python, JavaScript, Lisp, Smalltalk, Boo, you name it. The downside is that you get no language integration, so no nice syntax for contracts.

Code Contracts for .NET will be part of .NET 4.0 / Visual Studio 2010, but unfortunately there will be no DbC support in any of Microsoft's languages.

Darrickdarrill

So what makes you say that Spec# was abandoned? I can find no reference to this... – Anetteaneurin

I don't remember whether I heard that on a podcast, a Channel 9 video or maybe a blog post. Basically, nobody is working on Spec# anymore, because they all work full-time on the Code Contracts.NET library now. There might be bugfixes and maintenance releases for Spec#, but there won't be any ... – Protoactinium

... further development, there won't be a production release (currently it is illegal to use Spec# for commercial projects), and there most certainly won't be any C# 3.0 or C# 4.0 features. All the technology that was developed for Spec# is now in Code Contracts. – Protoactinium

Also, there has been no release since 2007. – Protoactinium

The relationship is explained a little bit here: Research.Microsoft.Com/Contracts/faq.aspx – Protoactinium