Author :
Christopher Swenson
Date :
2015-02-27 14:55:49
Hash :9b987f8c Message :Fix timsort invariant loop re: Envisage article
See http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/
We use a "runLen" array of size 128, so it should be nearly impossible
to have our implementation overflow.
But in any case, the fix is relatively simple -- checking two extra
conditions in the invariant calculation.
I also took this opportunity to remove some redundancy in the
left/right merge logic in the invariant loop.
Christopher Swenson