[Spark2014-discuss] Loop invariant for bubble sort

Hugues Jérôme hugues.jerome at gmail.com
Wed Jul 2 21:49:48 CEST 2014


Hi John,

Le 2 juil. 2014 à 21:36, John McCormick <mccormick at cs.uni.edu> a écrit :

> 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