none
Calling a method in Contract.Requires

    Question

  • Hi,
    Thanks for giving us an early look at Code Contracts - I've been following this since Spec#.
    I must also say that I prefer what we've got now over Spec#: it doesn't pollute the language and language agnostic too.

    My problem is that I've got the following method:
    public int Divide( int number, int divisor)
    {
        Contract.Requires( numberGreaterThanZero(divisor) );
        return number/divisor ;
    }

    [Pure]
    bool numberGreaterThanZero( int divisor )
    {
        return divisor > 0 ;
    }

    This always fails analysis.  If inline the method, it works fine.

    Is this a known bug?

    Cheers,

    Steve Dunn
    blog.dunnhq.com

    Sunday, March 08, 2009 12:26 PM

Answers

  • Thanks, now I understand the issue. In order for the static checker to understand the meaning of "numberGreaterThanZero", you need to write a contract on it as follows:

        [Pure]  
        public static bool numberGreaterThanZero(int divisor)  
        {  
          Contract.Ensures(Contract.Result<bool>() && divisor > 0 || !Contract.Result<bool>() && divisor <= 0);  
     
          return divisor > 0;  
        }  
     
    The contract essentially says exactly what the method does in this case, since it is such a simple method.

    Now, with this contract, the following tests should pass:

        public void Test()  
        {  
          this.Divide(100, 1);  
        }  
     
        public void Test2(int divisor)  
        {  
          Contract.Requires(numberGreaterThanZero(divisor));  
     
          var result = this.Divide(100, divisor);  
          Contract.Assert(result >= 0);  
        }  
     
        public int Divide(int number, int divisor)  
        {  
          Contract.Requires(numberGreaterThanZero(divisor));  
          Contract.Ensures(number < 0 || Contract.Result<int>() >= 0);  
     
          Contract.Assert(divisor > 0);  
          return number / divisor;  
        }  
     

    Note that I threw in some extra contracts for fun to see that we can really show that if the number is also non-negative, then Divide will return a non-negative result.

    Cheers, -MaF (Manuel Fahndrich)
    Monday, March 09, 2009 3:48 PM

All replies

  • Hi Steve, thanks for the feedback and I'm sorry you ran into a problem.

    Could you be more specific in terms of what fails? Is the runtime check failing each time? Please give us complete repro steps so we can investigate.

    Also, you probably want to make your "numberGreaterThanZero" predicate static.

    Thanks again,



    Cheers, -MaF (Manuel Fahndrich)
    Sunday, March 08, 2009 6:52 PM
  • Hi Manuel,
    Analysis fails with:
     warning : contracts: requires unproven (for myClass.Divide( 100, 1 ) ;), and warning :   + location related to previous warning (for Contract.Requires( numberGreaterThanZero(divisor) );).

    Making the method static didn't help.

    Many thanks,

    Steve
    Monday, March 09, 2009 6:42 AM
  • Thanks, now I understand the issue. In order for the static checker to understand the meaning of "numberGreaterThanZero", you need to write a contract on it as follows:

        [Pure]  
        public static bool numberGreaterThanZero(int divisor)  
        {  
          Contract.Ensures(Contract.Result<bool>() && divisor > 0 || !Contract.Result<bool>() && divisor <= 0);  
     
          return divisor > 0;  
        }  
     
    The contract essentially says exactly what the method does in this case, since it is such a simple method.

    Now, with this contract, the following tests should pass:

        public void Test()  
        {  
          this.Divide(100, 1);  
        }  
     
        public void Test2(int divisor)  
        {  
          Contract.Requires(numberGreaterThanZero(divisor));  
     
          var result = this.Divide(100, divisor);  
          Contract.Assert(result >= 0);  
        }  
     
        public int Divide(int number, int divisor)  
        {  
          Contract.Requires(numberGreaterThanZero(divisor));  
          Contract.Ensures(number < 0 || Contract.Result<int>() >= 0);  
     
          Contract.Assert(divisor > 0);  
          return number / divisor;  
        }  
     

    Note that I threw in some extra contracts for fun to see that we can really show that if the number is also non-negative, then Divide will return a non-negative result.

    Cheers, -MaF (Manuel Fahndrich)
    Monday, March 09, 2009 3:48 PM
  • Thanks Manuel,
    You say the static checker needs to understand the meaning of the "numberGreaterThanZero":  in this simple example, the contract IS the entire function, in fact, the code itself (return divisor > 0) even seems redundant after the contract!

    Is it not possible for it to just accept that a method returns a bool?  If not, there seems to be a limit to the complexity one can use.  Incidentally, would you know why string.IsNullOrEmpty from the BCL works?  Has this been 'contractified' some place?

    Cheers,

    Steve
    Thursday, March 12, 2009 7:02 AM
  • Hi Steve,

    What you say about the code and the contract of numberGreaterThanZero being the same is true. It is of course true that in general, contracts and code are in some way redundant expressions of each other. If contracts specified the complete functional behavior and also side effects (something that is difficult in general), then the method code and the contract would be completely redundant. One would only need one. For your simple function, this is the case.

    Now, inferring the post condition of this method is possible, and in fact we do have the option to do so: try to add -infer ensures on the extra options line in the contract property pane for the static checker. This might do it. I haven't checked.

    The problem with inference is that the inferred contracts are only visible in the same dll and it doesn't work for interfaces/virtual/abstract methods. So, even if it works in your dll above, if you call numberGreaterThanZero from another assembly, it wouldn't see the contract.

    As for your question about IsNullOrEmpty, we did indeed write contracts on it.

    Cheers, -MaF (Manuel Fahndrich)
    Friday, March 13, 2009 3:50 AM