我想在C#中实现DBC.我面对的是Spec#和Code Contract.
Spec#和Code Contract有什么区别？

解决方法:

这是从Code Contracts FAQs at Microsoft Research：

Do Code Contracts have anything to do with Spec#?

Code Contracts is a spin-off from the Spec# project. Spec#’s research focus is to
understand the meaning of object invariants in the presence of
inheritance, call backs, aliasing and multi-threading. Spec# is a
superset of C# v2.0 and uses a source level rewriter to weave the
contracts into the code. It uses verification condition generation and
a theorem prover for the static verification of Spec# code. But
dealing soundly with all the complex issues around maintaining object
invariants has a price: verification becomes non-trivial. That’s why
Spec# also needs an ownership discipline to know which objects may
alias or cannot alias each other.

Code Contracts is the result of learning from Spec# what works and
what doesn’t. Unlike Spec#, Code Contracts are language agnostic, and
thus work across all .NET languages, from VB to C# to F#. The rewriter
works on MSIL and thus had no dependency on particular compilers. Its
static analysis engine uses abstract interpretation, which is much
faster and more predictable than verification; furthermore abstract
interpretation infers loop invariants and method contracts, which
helps in adoption and ease of use of Code Contracts.

因此,代码合约似乎将成为未来更“支持”的工具.