2

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)

TamaMcGlinn
  • 2,840
  • 23
  • 34
MWB
  • 11,740
  • 6
  • 46
  • 91
  • 3
    Yes, SPARK can do it. You can look at some examples of formally verified sorting algorithms [here](https://github.com/tofgarion/spark-by-example/tree/Community2018/classic-sorting) (there is no Quickcheck there though). – aztek Mar 22 '21 at 22:36
  • 1
    SPARK is a tool. It’s up to the user to use it to prove {whatever}. Personal opinion: this is difficult, especially if you don’t have the training: see [here](https://blog.adacore.com/verifythis-challenge-in-spark). – Simon Wright Mar 23 '21 at 09:06
  • @SimonWright Thanks, although that is an `O(n^2)` sort. – MWB Mar 23 '21 at 19:01
  • I was thinking about the complexity of actually proving something not apparently very complex. Not necessarily related to the performance of the algorithm. – Simon Wright Mar 23 '21 at 20:16
  • @SimonWright I suspect they chose a slow algorithm because Quicksort was too hard. – MWB Mar 23 '21 at 20:19

1 Answers1

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]

Shark8
  • 4,095
  • 1
  • 17
  • 31