Language Supported Contracts (require)

[mirhagk]

As mentioned in #98 it'd be nice to have dedicated syntax and compiler support for pre-post conditions.

I like the use of the require *expr*. I'd like to see it done in a future-compatible, extendable way. For the simple case require name!=null will just compile to something like:

if (name!=null) throw new ContractViolation()

require should be allowed at the beginning of the method (perhaps even before the {) signifying it's a pre-condition, anywhere inside the method (in which case it's a condition that basically confirms that some code that just run acted like it should) or after the method (in which case it's wrapped in try{} finally{}) for a post-condition.

Pre/Post conditions (as well as the inline ones) are really only powerful when combined with static analysis tools.

Since determining when a given pre/post condition will be violated is a non-trivial task, the compiler should perhaps reduce itself to only checking the very trivial ones (when a constant violates the pre-condition for example). Language services can be used to provide warnings and errors for more involved cases, since they can be changed and updated much more frequently.

The conditions should also be eliminated when it can be statically proven that they are not needed at run-time. (There should also be a compile time flag to remove all if performance is desired over proven correctness, or if they trust the static analyzers enough). These need not be specified in the language spec (and hence doesn't force mono or others to implement them) but rather should be treated as an optimization detail (since if they can be statically proven to be not needed, then it does not change the semantics of the program).

This should allow the require tags to be forwards compatible, and not require breaking changes in the future when it's decided that more analysis can be done (as would have to be done now if more local type inference wanted to be introduced).

[stephentoub]

Thanks, @mirhagk. We've posted the proposal we were discussing in #98 as #119.

[Joe4evr]

As an aside, I believe your example should be:
if (name==null) throw new ContractViolation()

[mirhagk]

Okay I'm closing this issue because it looks like everything I wanted is included in the proposal. Just wanted to try and get the discussion out of #98 but you beat me to it.

EDIT: Also @Joe4evr yes you are right