Geek Answers Handbook

Contracts with C # code: Why can't this simple condition be proven?

I am doing a simple Code Contracts test. The following code is in winform. This goes (of course):

private void Test(Form form) { Contract.Requires(!string.IsNullOrEmpty(form.Name)); MessageBox.Show(form.Name); } protected override void OnLoad(EventArgs e) { if (!string.IsNullOrEmpty(Name)) Test(this); base.OnLoad(e); }

However, I add only a very simple level of indirection, he says: “requires unproven”:

  private bool Valid(string str) { return !string.IsNullOrEmpty(str); } protected override void OnLoad(EventArgs e) { if (Valid(Name)) Test(this); base.OnLoad(e); }

It seems to be trivial to prove. Why doesn't it work?

+4
source share
2 answers

Your Valid method has no contracts. You could have signed a contract there that would probably be exactly the same as the code, really ... but Codex Contracts are not going to allow that. Your implementation may change - you did not tell Code Contracts what this method should do, so it does not involve anything from the implementation.

+6
source

Do you really need a method just to call string.IsNullOrEmpty(str) ? And since String.IsNullOrEmpty(string) already marked as [Pure] in BCL, and since the shell is extraneous, the whole problem will simply disappear if you call it directly.

If you really take this method very strongly, then one of the ways this can work with your current code is to change the contract according to your Test method:

 private void Test(Form form) { Contract.Requires(Valid(form.Name)); MessageBox.Show(form.Name); } [Pure] private bool Valid(string str) { return !string.IsNullOrEmpty(str); }

Now the static analyzer should not complain.

+1
source

More articles:


All Articles