about Code Contracts - Language agnostic modular program verification and repair with abstract interpretation.
Code Contracts provide a language-agnostic solution to the problem of software specification and validation. They consist of an API (part of .NET) to author contracts, and several tools consuming it (e.g., code documentation, runtime checking, and static checking). The static checker, based on abstract interpretation, infers semantic facts and uses them to prove contracts, programmer-provided and language assertions. Furthermore, it helps the development process by providing verified code repairs.