I want to implement the DBC in C#. I faced with the Spec# and Code Contract for it.
What is the difference between Spec# and Code Contract?
This is from the 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.
So, it seems that Code Contracts would be the more 'supported' tool going forward.