SE547: Homework 8

Deadline: 5.30pm, Thursday 4 March 2004.

Homework

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.