Exercise 3

In this exercise, you will write some WhyML code of your own (instead of just reasoning about it).

As in the previous exercise, hand in your work as a .zip or tarball containing all relevant Why3 files, together with a report.txt detailing your findings (good and bad).

Task: implement a verified array sorting algorithm

You are going to (hopefully) verify a simple sorting algorithm. Choose either:

  1. Selection sort

  2. Insertion sort

  3. Bubble sort

You are assumed to be familiar with these algorithms, but feel free to look them up. You can either implement them in WhyML directly, but it is also okay to take a reference implementation in your favourite programming language and translate that into WhyML. In that case, please include it in your tarball or provide a reference.

Note that for an algorithm to be a sorting algorithm, it has to meet three criteria:

Instructions

  1. Pick a sorting algorithm and implement it in WhyML. These sorting algorithms are typically presented as one "large" function with nested loops, but you can also decide to use multiple functions instead.

    Make sure that your main sorting function has this signature:

    let sort(a: array int)
  writes { a }
= (* ... *)

  2. Invent a postcondition that expresses the fact that the array will be sorted when sort is done.

  3. Prove that your sorting algorithm satisfies this postcondition by finding (and proving) invariants, as well as suitable contracts of any auxilliary functions you may have created.

  4. If you have any proof obligations for program termination, add variants to prove that your program terminates.

  5. Add a postcondition that expresses the fact that the sorted array has exactly the same elements as the input (i.e., that it is a permutation of the original array).

  6. Prove this postcondition as in step 3.

Hints