Is D's TimSort correct?

[ketmar via Digitalmars-d]

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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: not available
URL: <http://lists.puremagic.com/pipermail/digitalmars-d/attachments/20150224/a1dc96d0/attachment.sig>