[Spark2014-discuss] Loop invariant for bubble sort

Yannick Moy moy at adacore.com
Thu Jul 3 09:46:37 CEST 2014


-- Claude Marche (2014-07-02)
> 
>> 
>> 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. 
> 
> This is just incredible. The Why3 version of selection sort is proved in
> no time by Alt-Ergo, see
> 
> http://toccata.lri.fr/gallery/selection_sort.en.html
> 
> This deserves to be investigated.

There are two main differences:
- you're using in Why3 axiomatized libraries for sortedness and permutation, which are not currently available for SPARK
- the encoding of Ada types into Why3 gives more work to provers (for example, bounded integers to math integers)

BTW, Claire could prove John's program in a few minutes with Alt-Ergo + CVC4 + Z3. But no prover alone currently achieves the same.
--
Yannick Moy, Senior Software Engineer, AdaCore






More information about the Spark2014-discuss mailing list