Can SPARK be used to prove that Quicksort actually sorts?

Question

I'm not a user of SPARK. I'm just trying to understand the capabilities of the language.

Can SPARK be used to prove, for example, that Quicksort actually sorts the array given to it?

(Would love to see an example, assuming this is simple)

Answer 1

Yes, it can, though I'm not particularly good at SPARK-proving (yet). Here's how quick-sort works:

1. We note that the idea behind quicksort is partitioning.
2. A 'pivot' is selected and this is used to partition the collection into three groups: equal-to, less-than, and greater-than. (This ordering impacts the procedure below; I'm using this because it's different than the in-order version to illustrate that it is primarily about grouping, not ordering.)
3. If the collection is 0 or 1 in length, then you are sorted; if 2 then check and possibly-correct the ordering and they are sorted; otherwise continue on.
4. Move the pivot to the first position.
5. Scan from the second position position to the last position, depending on the value under consideration:
   1. Less – Swap with the first item in the Greater partition.
   2. Greater – Null-op.
   3. Equal — Swap with the first item of Less, the swap with the first item of Greater.
6. Recursively call on the Less & Greater partitions.
7. If a function return Less & Equal & Greater, if a procedure re-arrange the in out input to that ordering.

Here's how you would go about doing things:

1. Prove/assert the 0 and 1 cases as true,
2. Prove your handling of 2 items,
3. Prove that given an input-collection and pivot there are a set of three values (L,E,G) which are the count of the elements less-than/equal-to/greater-than the pivot [this is probably a ghost-subprogram],
4. Prove that L+E+G equals the length of your collection,
5. Prove [in the post-condition] that given the pivot and (L,E,G) tuple, the output conforms to L items less-than the pivot followed by E items which are equal, and then G items that are greater.

And that should do it. [IIUC]