<story><title>Proving that Android’s, Java’s and Python’s sorting algorithm is broken</title><url>http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/</url></story><parent_chain><item><author>stingraycharles</author><text>In the Haskell community there is a tool called QuickCheck [1]: it is able to generate inputs based on preconditions, and you provide a function to verify the postconditions.&lt;p&gt;I am not sure why these kind of testing methods aren&amp;#x27;t used more often in other communities, since it makes it really easy to catch corner cases; in the Haskell world, at least, using QuickCheck is somewhat pervasive.&lt;p&gt;[1] &lt;a href=&quot;https://wiki.haskell.org/Introduction_to_QuickCheck2&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;wiki.haskell.org&amp;#x2F;Introduction_to_QuickCheck2&lt;/a&gt;&lt;p&gt;EDIT: I have never done this before, but could anyone explain why I am being downvoted? I wasn&amp;#x27;t making the claim that this is a substitute for a formal proof, I was merely adding this information to the discussion since it seemed relevant.</text></item><item><author>thomasahle</author><text>This is actually really cool. They tried to verify Timsort as implemented in Python and Java using formal methods. When it didn&amp;#x27;t seem to work, they discovered that there was actually a missing case in both implementations, which could lead to array out of bounds exceptions.&lt;p&gt;Really shines as an example of how important proof is in computer science.</text></item></parent_chain><comment><author>grandpa</author><text>There&amp;#x27;s a difference, though: QuickCheck randomly tries a large-ish number of possible inputs to try and disprove a postcondition, whereas formal methods prove the postcondition for all inputs.  Practically, if the number of possible inputs is huge compared to the number of failure cases, it&amp;#x27;s unlikely that QuickCheck will find it.  I strongly suspect - and this would be an interesting experiment - that QuickCheck wouldn&amp;#x27;t have found this particular bug, since Timsort has been in use for years without anyone noticing it.</text></comment>
<story><title>Proving that Android’s, Java’s and Python’s sorting algorithm is broken</title><url>http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/</url></story><parent_chain><item><author>stingraycharles</author><text>In the Haskell community there is a tool called QuickCheck [1]: it is able to generate inputs based on preconditions, and you provide a function to verify the postconditions.&lt;p&gt;I am not sure why these kind of testing methods aren&amp;#x27;t used more often in other communities, since it makes it really easy to catch corner cases; in the Haskell world, at least, using QuickCheck is somewhat pervasive.&lt;p&gt;[1] &lt;a href=&quot;https://wiki.haskell.org/Introduction_to_QuickCheck2&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;wiki.haskell.org&amp;#x2F;Introduction_to_QuickCheck2&lt;/a&gt;&lt;p&gt;EDIT: I have never done this before, but could anyone explain why I am being downvoted? I wasn&amp;#x27;t making the claim that this is a substitute for a formal proof, I was merely adding this information to the discussion since it seemed relevant.</text></item><item><author>thomasahle</author><text>This is actually really cool. They tried to verify Timsort as implemented in Python and Java using formal methods. When it didn&amp;#x27;t seem to work, they discovered that there was actually a missing case in both implementations, which could lead to array out of bounds exceptions.&lt;p&gt;Really shines as an example of how important proof is in computer science.</text></item></parent_chain><comment><author>im3w1l</author><text>It wouldn&amp;#x27;t catch this bug. The algorithm works for lists of size less than 2^49.</text></comment>