[Spark2014-discuss] Loop invariant for bubble sort

John McCormick mccormick at cs.uni.edu
Wed Jul 2 22:08:57 CEST 2014

I'm working on the selection sort out of my data structures textbook.  I 
haven't looked at the one proposed on the SPARK2014 blog.

On 7/2/2014 2:49 PM, Hugues Jérôme wrote:
>> My selection sort invariants for ordering and partitioning took nearly an hour to prove with alt-ergo.  If you are convinced that your assertions are correct (tested with assertions enabled),  you might want to do a proof run overnight or try alternate provers.
> Thanks for the time estimation. I did not suspect it could reach such limits for sorting algorithms.
> Out of curiosity, which implementation did you prove? The one proposed on SPARK2014 blog or your own? I’ll some time to test tomorrow morning. Thanks!

More information about the Spark2014-discuss mailing list