Is Spec# stable enough to use? [closed]

2020-02-09 13:56发布

问题:

This question is unlikely to help any future visitors; it is only relevant to a small geographic area, a specific moment in time, or an extraordinarily narrow situation that is not generally applicable to the worldwide audience of the internet. For help making this question more broadly applicable, visit the help center.
Closed 7 years ago.

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?

回答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.