none
Will you ever support IComparable and IComparable<T>?

    질문

  • Hello,

    I wonder whether you will add support for this because currently it's not possible to do the following

    [ContractAbbreviator]
    public static void LessThan<T>(T upperBound) where T : IComparable<T>
    {
    	Contract.Ensures(Contract.Result<T>().CompareTo(upperBound)  < 0);
    }

    although this is working fine.

    [ContractAbbreviator]
    public static void LessThan(int upperBound)
    {
    	Contract.Ensures(Contract.Result<int>() < upperBound);
    }
    it can save a lot of work and in my opinion is a lot nicer.


    Regards,

    Eyal Shilony

    2012년 8월 6일 월요일 오전 1:14

모든 응답

  • I'm just wondering, is it a technical limitation that prevents you from supporting this? or a design decision? I've searched high and low and found nothing about it so please elaborate.


    Regards,

    Eyal Shilony

    2012년 8월 6일 월요일 오전 5:50
  • What do you mean by "support this"? What doesn't work with the former example?

    Mike Barnett

    2012년 8월 6일 월요일 오후 2:44
  • The static checker can't verify it or it does but issue warnings for it.

    Regards,

    Eyal Shilony

    • 편집됨 Eyal Shilony 2012년 8월 7일 화요일 오전 5:30
    2012년 8월 6일 월요일 오후 2:47
  • Is there any progress on this?

    I've been waiting for an answer for so long, please tell me what is the reason the former doesn't work? here is another thread of mine with similar issue.

    Edit: I'm not certain, it might be something that I overlook on my part and this is actually working but I haven't realised it yet.


    Regards,

    Eyal Shilony

    • 편집됨 Eyal Shilony 2012년 9월 11일 화요일 오후 3:01
    2012년 9월 11일 화요일 오전 1:18
  • It looks as if the static checker doesn't know enough about CompareTo. The following code verifies for me, but without the assumption, the checker complains about not being able to prove the postcondition it gets from the abbreviator.

     class C {
        [ContractAbbreviator]
        public static void LessThan<T>(T upperBound) where T : IComparable<T> {
          Contract.Ensures(Contract.Result<T>().CompareTo(upperBound) < 0);
        }
    
        public char MyCompare(char c) {
          LessThan(c);
          Contract.Ensures(Contract.Result<char>() == 'b');
          Contract.Assume('b'.CompareTo(c) < 0);
          return'b' ;
        }
      }

    2012년 9월 11일 화요일 오후 3:53
  • Sure! you should grasp what's going on from the sample I made, there are some tests in the Tests class that demonstrate the issue.

    Edit: Mike, can't you guys do something about it? because I don't think that adding these assertions is ideal.


    Regards,

    Eyal Shilony

    • 편집됨 Eyal Shilony 2012년 9월 11일 화요일 오후 5:42
    2012년 9월 11일 화요일 오후 5:29
  • When you say "adding these assertions", do you mean the ones from your sample like Assert.GreaterThan?

    You labeled that one as "working", but I'm not sure that is really working. The checker does not understand tht GetNonZeroNumber returns a positive number. If you modify the method Working_as_intended so that following the call to GetNonZeroNumber you have "Contract.Assert(0 < n);", you will see that the checker cannot prove it. The reason it is not complaining about the postcondition of Working_as_intended is that it just takes the postcondition from Assert.GreaterThan and "inlines" it so that it knows n is greater than zero. It is just as if you had written "Contract.Assume(0 < n);" instead of the call to Assert.GreaterThan. It does the same for the generic version of GreaterThan, but then the assumption is just "n.CompareTo(0) > 0". Unfortunately, there are no contracts on IComparable<T>.CompareTo that would somehow relate that to the postcondition that needs to be proven, e.g., "result > 0". I've contacted Francesco to see what he can say about having the static checker understand this.

    The thing that I think *is* wrong is your method GreaterThan_cannot_be_proven. Even if I change the postcondition to "Contract.Ensures(Contract.Result<int>().CompareTo(0) > 0);" the checker is unable to prove the postcondition. I am forwarding that example to Francesco to look at.


    Mike Barnett

    2012년 9월 11일 화요일 오후 6:13
  • Mike, no, I referred to the assertions you added to your previous post in which you edit.

    I presume it's like you said 'IComparable<T>' and 'IComparable' do not have contracts on them so it can't handle these cases, I guess that's what I was asking for in my original post.

    Edit: I think I misread you so I removed the irrelevant bits from this post.


    Regards,

    Eyal Shilony

    • 편집됨 Eyal Shilony 2012년 9월 11일 화요일 오후 9:31
    2012년 9월 11일 화요일 오후 8:10