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)
Yes, it can, though I'm not particularly good at SPARK-proving (yet). Here's how quick-sort works:
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.Less
– Swap with the first item in the Greater
partition.Greater
– Null-op.Equal
— Swap with the first item of Less
, the swap with the first item of Greater
.Less
& Greater
partitions.Less
& Equal
& Greater
, if a procedure re-arrange the in out
input to that ordering.Here's how you would go about doing things:
0
and 1
cases as true,2
items,(L,E,G)
which are the count of the elements less-than/equal-to/greater-than the pivot [this is probably a ghost-subprogram],L
+E
+G
equals the length of your collection,(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]