*Deadline*: 5.30pm, Thursday 4 March 2004.

1. The file sort.c contains a finished implementation of bubblesort. You should edit this file, and change it to implement quicksort. Your quicksort algorithm should be in-place, and should take the middle element of the array as the pivot element. You should ensure that the program passes the cbmc validation for array bounds checks.

2. You should now write a function
`int sorted (int* array, int size)`

which tests to ensure that an array is sorted.
You should ensure that your implementation of quicksort
passes the test `assert (sorted (array, size));`

using cbmc. The test harness for this is:

#define SIZE 3 // Try increasing this number! void test () { int array[SIZE]; yourSortFunction (array, SIZE); assert (sorted (array, SIZE)); }

3. If you include the statement `assume (size < 5)`

in the `test`

function, you can then try to
find whether you can get cbmc to validate your program
without using the flag `--no-unwinding-assertions`

.
Can you manage to find a value for `--unwind`

which validates your program? If so, what is the value?
If not, discuss why.

Submit your answers as a C source file using Courses On Line.