Microsoft Research created Spec#, which extends C# to have Eiffel-style contracts (pre- and post-conditions) specified above a function body. While the requires

Microsoft Research created Spec#, which extends C# to have Eiffel-style contracts (pre- and post-conditions) specified above a function body. While the requires and ensures aren't dependent types, they do allow for extended static checking via Microsoft's Z3 theorem prover. http://en.wikipedia.org/wiki/Spec_Sharp http://en.wikipedia.org/wiki/Spec_Sharp