Code Contracts for
Code Contracts includes a static checker program for verifying both explicit and implicit (null references, array bounds, etc.) code contracts. Runtime (dynamic) contract checking can use marked series of If-Then-Throw guard clauses as in:
if ( x == null )
throw new ArgumentNullException("x");
if ( y < 0 )
throw new ArgumentOutOfRangeException(...);
(so you don't waste perfectly good guard clauses) as well as the standard, explicit code contracts like:
.y >= 0);
.x == 3,
"Why isn't the value of x 3?");
Contract.Requires(x ! = null,
"DANGER -- missles fired!");
Code Contracts defaults at runtime to throwing an exception (System.Diagnostics.Contracts.ContractException) when a contract is violated (this behavior is configurable).
I have not tried Code Contracts (or any code contract mechanism) yet, but the idea is intriguing because it lets the computer do something it does well (exhaustive examination of your code in tedious detail) thereby freeing you to work on the higher-level aspects of your program, just as C freed us from assembly language bookkeeping and Perl/Java/VB.NET etc. free us from C language bookkeeping.
If anyone has experience with code contracts for any language (positive or negative), please comment.