[Spark2014-discuss] Loop invariant for bubble sort
moy at adacore.com
Thu Jul 3 09:42:40 CEST 2014
-- Claude Marche (2014-07-03)
> Here is a Why3 version of bubble sort, fully proved with alt-ergo with a
> time limit of 5 seconds.
Note that this version conveniently uses the standard library of Why3 for axiomatizing sortedness and permutation properties:
use import array.IntArraySorted
use import array.ArraySwap
use import array.ArrayPermut
> Hope it will help you to design a Spark version of it. Keep us inform of
> your achievements !
Ideally, we should provide a similar SPARK standard library of generic sortedness/permutations functions, to facilitate user's work. Until then, the user of SPARK has to either come up with such a local library, or "inline" these properties in the loop invariants he/she writes.
Yannick Moy, Senior Software Engineer, AdaCore
More information about the Spark2014-discuss