Remove/replace unprovable contracts.

[tom-englert]

Some contracts that are theoretically valid but can't be proven by the static checker.
Crated issue #86, so once the checker is improved they can be enabled again.

[sharwell]

💡 I prefer these types of longer comment stay in the issue instead of the code. I've found that over time, code gets corrected but the comments tend to stay forever.

📝 The other inline comments you added at the location of commented calls to Contract.Requires below are different. They are short, and obviously would be changed if someone did implement support for these contracts in the future.

[mike-barnett]

I’m not sure if the best route here is to get rid of the contracts. If they are valid preconditions, but something that the static checker seems unable to prove at call sites (and I’m not sure how you are certain that is true), then you can always add a Contract.Assume just before the call site.

I also don’t understand why you have gotten rid of some postconditions. Why would you do that? The checker never tries to prove a postcondition except when it is verifying the implementation of a method. Are you saying that you are trying to run the static checker on the source of Mscorlib’s implementation?

Mike

From: tom-englert [mailto:[email protected]]
Sent: Friday, July 3, 2015 10:50 AM
To: Microsoft/CodeContracts
Subject: [CodeContracts] Remove/replace unproofable contracts. (#85)

Some contracts that are theoretically valid but can't be proofed by the static checker.

---

You can view, comment on, or merge this pull request online at:

#85

Commit Summary

• Disable Contract.Requires that the static checker can't prove.
• Contracts in System.Math that the checker can't proof.

File Changes

• M Microsoft.Research/Contracts/MsCorlib/System.Math.cshttps://github.com/Remove/replace unprovable contracts. #85/files#diff-0 (27)
• M Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cshttps://github.com/Remove/replace unprovable contracts. #85/files#diff-1 (41)
• M Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cshttps://github.com/Remove/replace unprovable contracts. #85/files#diff-2 (4)

Patch Links:

• https://github.com/Microsoft/CodeContracts/pull/85.patch
• https://github.com/Microsoft/CodeContracts/pull/85.diff

—
Reply to this email directly or view it on GitHubhttps://github.com//pull/85.

[tom-englert]

I mainly look at contracts from the users side, not from mathematical theory.
Contracts are a tool to help writing better code. If it hinders you from writing clean code (e.g. if there are more Contract.Assume statements than active code), something is wrong.
This happened to me with Rect and Size, which are heavily used e.g. in layout calculations. Code like

var r = new Rect();
Contract.Assume(!r.IsEmpty);
r.Width = 5;
Contract.Assume(!r.IsEmpty);
r.Height = 10;

is no longer readable. I won't find any acceptance in any team for using CC if people have to write code like this.

For the post conditions I did not remove them, but simplified them so something that the checker could understand. My reference here was that code like

var r = new Rect(0, 0, Math.Abs(a), Math.Abs(b))

should not generate a warning that width and height are unproven to be positive values. I could not convince anyone that it would be better to write the above statement in 10 lines, where 5 would be just Contract.Assume to make the checker happy.

It does not make sense building cars if there are no roads. Lets start making some good shoes, and do the cars when we have the roads.

[mike-barnett]

Ah, those are great points. Yes, I totally agree in general. But in this case, wouldn't it be better to add a postcondition to the constructor Rect that says it isn't empty? For the latter example, is it that Math.Abs lacks a postcondition or is it that the checker is not good at proving this because they are floating point numbers?

[tom-englert]

I have to get some practical sample code to see what was the issue with Size and Rect. Maybe decorating every method and property with Contract.Ensures(!this.IsEmpty) can fix this.

For Math.Abs I think it is the link between input and output, where it could not decide whether input was some infinity or not, so none of the existing ensures got active.

[tom-englert]

The main obstacle here is that Rect and Size are value types, so they can't have a parameterless constructor that could say Contract.Ensures(!this.IsEmpty). If I use e.g. new Rect(0,0,0,0) things look better.
So to fix this we would need

• a way to add contracts to the default constructor of value types
• someone who checks every method that returns a Rect or a Size and adds the Contract.Ensures(!Contract.Result<Rect/Size>().IsEmpty) if applicable. (would be a good job for a trainee)

[mike-barnett]

Oh, good point about having contracts on the nullary ctor for structs. Yes, I agree now with your changes to the contracts.

[tom-englert]

Created issue #98. (Add a possibility to add contracts to the default constructor of value types)

[tom-englert]

@mike-barnett any idea why the original contracts of Math.Abs don't work?
I'm not sure how the analyzer will handle multiple Contract.Ensures, so I can't tell if they are wrong or just too complex.

On the other hand: Would anyone gain any profit from the original implementation if it would work? Is it worth spending time on this?

[brettshearer]

I would expect that if the analyser has problems because the contracts are too complex then there may be benefit in improving the analyser, far outside of the Math.Abs problem.

From: tom-englert [mailto:[email protected]]
Sent: Thursday, 9 July 2015 5:30 PM
To: Microsoft/CodeContracts
Subject: Re: [CodeContracts] Remove/replace unprovable contracts. (#85)

@mike-barnetthttps://github.com/mike-barnett any idea why the original contracts of Math.Abs don't work?
I'm not sure how the analyzer will handle multiple Contract.Ensures, so I can't tell if they are wrong or just too complex.

On the other hand: Would anyone gain any profit from the original implementation if it would work? Is it worth spending time on this?

—
Reply to this email directly or view it on GitHubhttps://github.com//pull/85#issuecomment-119855505.

[mike-barnett]

I don't know details of why they don't work, but I know that the checker can have problems with floating point numbers. Multiple postconditions should be just fine: the checker just conjoins them all.

I'm not sure if it is that important at the moment. Maybe just comment out the contracts on Rect (and any similar structs) and leave a comment about why they aren't there.

[tom-englert]

OK, that's what the current state is, and we have two issues (#86, #98) to remind us to deal with this later.
@SergeyTeplyakov: So it seems to me this could be merged as well.

[sharwell]

❓ What happens if instead of commenting out these Ensures lines, just just add the new one above?

[tom-englert]

This would work as well, but I found this would be too confusing - if it's commented, it's more clear that it is not active at all.

[sharwell]

It only shows in the editor extensions quick info if it's active though. 😄 I created #104 to deal with this later since it was clear that you would benefit from having these changes in the first community preview.

[sharwell]

I understand removing IsEmpty from the Requires of several methods. I do want to understand two things before merging this though. The first question is added as a diff comment which appears above. The second is:

❓ What happens if instead of commenting out Contract.Requires(IsEmpty), we simply change it to Contract.Assume(IsEmpty)? I'm guessing it won't work, but if it does happen to work it would be an interesting way to preserve the semantic information.