[Spark2014-discuss] Loop invariant for bubble sort

Yannick Moy moy at adacore.com
Wed Jul 2 22:16:46 CEST 2014


-- John McCormick (2014-07-02)
> 
> 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.

Hi John,

I think it's the same code. Claire used the example you sent for experimenting with the assertional style of manual proof (see for example "An Assertional Proof of the Stability and Correctness of Natural Mergesort" as a recent example from Rustan Leino, a researcher who's been pushing this way of performing manual proofs for a few years now).

She's published the results of these experiments on SPARK 2014's blog:
http://www.spark-2014.org/entries/detail/manual-proof-in-spark-2014
--
Yannick Moy, Senior Software Engineer, AdaCore






More information about the Spark2014-discuss mailing list