Are Microsoft Code contracts not validating user input?

Question

I saw how it is written elsewhere on SO that while the Application Validation Application Enterprise block is for checking user inputs, Code Contracts are for preventing programmer errors. Would you support this opinion? Why?

Answer 1

Yes.

Code contracts are designed to maintain a rigorous programming interface that only a developer can get right or wrong; the user should not really mess it up.

Validation is designed to validate data; for example, data validation is not NULL or matches a regular expression.

Answer 2

Code contracts raise exceptions when they are violated. Invalid user input is not an exclusive condition, therefore, validation functions should not generally exclude exceptions. That's why methods like TryParse were added to the Framework (the original Framework did not have them, and this made validation cumbersome due to all possible exceptions).

Answer 3

Code contracts are used to assert things that will always be true, and if they are incorrect, then there is an error in the code. This means that it can only be applied to conditions that are controlled by code. Thus, you cannot use them to indicate "the user will never supply an empty string" because it is out of code control. A static verifier can never prove this statement - how can he know what the user will do?

What you can do is make expressions like "Given user input, the method will either return a non-empty string or throw an exception."