Practical verification for the working programmer with CodeContracts and Abstract Interpretation – Invited Talk

CodeContracts provide a language agnostic way to specify and check preconditions, postconditions and object invariants (collectively called contracts [17]). Specications take the form of calls to static methods of a Contract library [7]. The authoring library is available out-of-the-box to all .NET programmers from v4.