[Spark2014-discuss] Loop invariant for bubble sort
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