Some implementation out there are buggy:


http://www.reddit.com/r/programming/comments/2wze7z/proving_that_androids_javas_and_pythons_sorting/

Ali

On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:

> Some implementation out there are buggy:
> 
> 
> http://www.reddit.com/r/programming/comments/2wze7z/
proving_that_androids_javas_and_pythons_sorting/
> 
> Ali

their KeY system is very interesting. i'm very curious what minimal changes can be made for D to integrate something like it into the source code. i.e. turn all that pseudo-comment things that KeY is using into valid D code. compiler can check code semantics, so all contracts are at least syntactically correct. and then KeY-like tool can try to prove the correctness.

we already has `in` and `out`, and `invariant` for structs/classes. i believe that `invariant` can be reused for other invariants (like loop invariant)...

and it's interesting what complications templates can bring. testing templates is relatively hard now, 'cause programmer must ensure that every path is instantiated (i'm constantly hitting by the bugs in my templates due to missing some codepathes).

sorry for derailing the thread.

On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:

> Some implementation out there are buggy:
> 
> 
> http://www.reddit.com/r/programming/comments/2wze7z/
proving_that_androids_javas_and_pythons_sorting/
> 
> Ali

p.s. and yes, `TimSortImpl` is broken.

On 02/24/2015 11:15 AM, ketmar wrote:

> and it's interesting what complications templates can bring. testing
> templates is relatively hard now, 'cause programmer must ensure that
> every path is instantiated (i'm constantly hitting by the bugs in my
> templates due to missing some codepathes).

I was going to suggest dmd's code coverage tool but I've just witnessed the problem first-hand: Uninstantiated template code is not visible to the coverage analyser! :-o

Here is the program, where the code inside 'static if' is not covered (because argument 'a' is char):

T foo(T)(T v)
{
    static if (T.sizeof == 4) {
        ++v;
    }

    return v;
}

void main()
{
    int a = foo('a');
}

$ dmd deneme.d -cov
$ ./deneme
$ tail --lines=14 deneme.lst
       |T foo(T)(T v)
       |{
       |    static if (T.sizeof == 4) {
       |        ++v;
       |    }
       |
      1|    return v;
       |}
       |
       |void main()
       |{
      1|    int a = foo('a');
       |}
deneme.d is 100% covered

Yay! 100% covered. WAT? :p

Ali

On Tue, 24 Feb 2015 11:48:37 -0800, Ali Çehreli wrote:

> I was going to suggest dmd's code coverage tool but I've just witnessed the problem first-hand: Uninstantiated template code is not visible to the coverage analyser! :-o

yes. i don't think that this is a bug, though: coverage analyser analyses only actually existing code, and non-instantiated template is inexisting. ;-)

and forcing compiler to instantiate all possible template variants is both impractical and not even possible, i think.

yet symbolic checker like KeY can be very handy here, i think. it can prove that some instantiations are effectively the same, for example.

On 02/24/2015 11:20 AM, ketmar wrote:
> On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:
>
>> Some implementation out there are buggy:
>>
>>
>> http://www.reddit.com/r/programming/comments/2wze7z/
> proving_that_androids_javas_and_pythons_sorting/
>>
>> Ali
>
> p.s. and yes, `TimSortImpl` is broken.
>

Thanks. Posted:

  https://issues.dlang.org/show_bug.cgi?id=14223

Ali

On Tue, 24 Feb 2015 13:35:09 -0800, Ali Çehreli wrote:

> On 02/24/2015 11:20 AM, ketmar wrote:
>> On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:
>>
>>> Some implementation out there are buggy:
>>>
>>>
>>> http://www.reddit.com/r/programming/comments/2wze7z/
>> proving_that_androids_javas_and_pythons_sorting/
>>>
>>> Ali
>>
>> p.s. and yes, `TimSortImpl` is broken.
>>
>>
> Thanks. Posted:
> 
>    https://issues.dlang.org/show_bug.cgi?id=14223

i added a quick patch there. it would be fine if someone will run unittests (and add a unittest for the case from the article), 'cause i just did a mechanical translation of the fix without deep code analysing.

On Tuesday, 24 February 2015 at 21:35:10 UTC, Ali Çehreli wrote:
> On 02/24/2015 11:20 AM, ketmar wrote:
>> On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:
>>
>>> Some implementation out there are buggy:
>>>
>>>
>>> http://www.reddit.com/r/programming/comments/2wze7z/
>> proving_that_androids_javas_and_pythons_sorting/
>>>
>>> Ali
>>
>> p.s. and yes, `TimSortImpl` is broken.
>>
>
> Thanks. Posted:
>
>   https://issues.dlang.org/show_bug.cgi?id=14223
>
> Ali

Beware, as commented on the original article, then linked on reddit and relinked here ( http://www.reddit.com/r/programming/comments/2wze7z/proving_that_androids_javas_and_pythons_sorting/cow0de5 ) most of the proposed "fix" have the same issue as the blamed ode in the first place.

On Tue, 24 Feb 2015 19:20:08 +0000, ketmar wrote:

> On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:
> 
>> Some implementation out there are buggy:
>> 
>> 
>> http://www.reddit.com/r/programming/comments/2wze7z/
> proving_that_androids_javas_and_pythons_sorting/
>> 
>> Ali
> 
> p.s. and yes, `TimSortImpl` is broken.

p.p.s. i can't really check that java code (it OOMs), and i supposed "brokenness" from simply reading `TimSortImpl` (as it uses the same algorithm as other implementations). so far it seems that to hit the bug the arrays must be extraordinarily huge, so there is no need to take an urgent action.