I was wondering if I'm able to use Microsoft Code Contracts to verify the invariant that a method shall not throw any exception. The use case is as follows: I have an importer with a logger attached to it, where the importer uses a base class for the importer defining various phases of the import:
Each phase is represented by an abstract method of that importer base class. I'd like to ensure as invariant for each phase that it does not throw any documented exceptions. Ergo, the "Read a file" phase should handle all file access related problems (DirectoryNotFoundException for example), logging the problem with the logger and returning null.
In essence, we want to channel problems via the logger. And based on the severity of the problem, abort the import, continue while ignoring the problem.
I've read the manual quickly, but haven't found anything that seems usable for this. Is it at all possible? Or is it not possible and there is actually a very good reason for it that I'm missing?
I don't think it's possible to verify it doesn't throw any exception, because exceptions can originate from the runtime itself; consider OutOfMemoryException or StackOverflowException.
In fact, I think this is why it's hard in the general case - if you're using exceptions correctly then they will usually be caused by external inputs to the program, and so cannot be verified.
(If the exception would be caused by a bug in the program, then you could probably use pre-conditions to catch that)
Actually, come to think of it, there's already a compiler-supported way of verifying that exceptions are thrown or handled... just not in .NET :D. Java's checked exceptions would seem to satisfy your use case, but even Java's own community seem to think they were a bad idea nowadays.