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