[Spark2014-discuss] Loop invariant for bubble sort

Yannick Moy moy at adacore.com
Thu Jul 3 09:42:40 CEST 2014

-- Claude Marche (2014-07-03)
> Hi,
> 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 mailing list