search

microsoft / CodeContracts

Source code for the CodeContracts tools for .NET
Other
882 stars 151 forks source link

Unprovable contracts #86

Open tom-englert opened 9 years ago

tom-englert commented 9 years ago

There are some system contracts that the static checker can't cope with since they are too complex. These contracts have been disabled in https://github.com/Microsoft/CodeContracts/pull/85, because they generate false warnings that are not fixable in source code.

e.g. in Rect the requirement Contract.Requires(!this.IsEmpty) is true, but it's impossible to proof with acceptable effort. Even simple code like var r = new Rect(); r.Widht = 10.0; will create a warning "CodeContracts: requires unproven: !this.IsEmpty. Are you making some assumption on get_Width that the static checker is unaware of?"

Once we can find a way how the checker can proof these contracts we might enable them again.

sharwell commented 9 years ago

:thought_balloon: For immutable value types (e.g. Rect), it would be nice to have a way to mark that the value of a method or property is not only pure, but also will never change result over the life of the object. This annotation would allow a trait such as Contract.Assume(rect.IsEmpty) to be propagated more efficiently with the instance (once IsEmpty => always IsEmpty).