May we get an example of such proof in those languages? Because formal proof isn't something people talk about often, so most of us are not familiar with this.
I'll give it a try.
First, let's prove that our algorithm is correct. An example: how do we prove quicksort:
An array is sorted if and only if each element is not smaller than any of the preceeding elements. (And not larger than any of the following elements, which is an obvious consequence).
Let's prove that quicksort gives a sorted array on its output. It is obvious that an array of only one element is always sorted. On each step of quicksort we split the array so that the first part contains only elements not larger than the pivot and the second has only larger elements. That means, any element of second subarray is not smaller as any element of the first one. Since it is not smaller than the pivot, this operation does not affect the "sorted" property: if both subarrays are sorted, so is the result. By mathematical induction, this means that the algorithm makes sorted array for any number of elements. Proven.
Now let's prove that our implementation is really the correct implementation of the proven algorithm. For illustrative purposes, I make a very inefficient C99 implementation:
void quicksort(int data[], size_t size)
{
if (size < 2)
return;
const int pivot = data[0];
int left[size];
size_t left_size = 0;
int right[size];
size_t right_size = 0;
for (size_t i = 1; i < size; ++i)
{
if (data[i] <= pivot)
{
left[left_size++] = data[i];
}
else
{
right[right_size++] = data[i];
}
}
quicksort(left, left_size);
quicksort(right, right_size);
for (size_t i = 0; i < left_size; ++i)
data[i] = left[i];
data[left_size] = pivot;
for (size_t i = 0; i < right_size; ++i)
data[i + left_size + 1] = right[i];
}
I wrote it so that there is some place for errors, but we can still prove that it is correct (to some extents, see below).
If size < 2, this means, that the array has only one or zero elements, It is already sorted. Do nothing. Ok.
We choose very first element as a pivot. Ok.
We create two arrays and their sizes. This is the place where our program can fail if there is not enough stack memory. Here we have no guard against it, and we have to proof elsewhere that our array size is small enough to fit our stack. In the worst case we'll need at least size*(size+1)*sizeof(int) stack space + size recursion depth. Let's consider here that we have a proof of having such a stack space to the point of the call. Ok.
Then we loop for the rest of elements, started at the second one. This loops guarantees that each element is going to the left or to the right (but not both), and all elements not larger than the pivot are going to the left. This means, left and right will have the property required by our theoretical proof, and sum of their sizes wull be exactly size-1. Ok.
Call quicksort twice. Ok.
Copy elements from the left. Such copying takes exactly one element and keeps their amount and order. Ok.
Copy pivot. Pivot should go after the left array. Ok.
Copy right side. Here we should check array indices carefully. We could see that, if i = 0, our element goes right after pivot. And the index of the last element is size - 1 + left_size + right_size + 1 = size - 1, which is correct too. Ok.
Proven, with the exception of stack size problem.
A general rule here is: "I do not write what I can't prove". Not every code can be proven in such a way. This is the matter of human discipline. No technology is completely fool-proof.
Functional languages like Lisp and languages like Ada are designed to make such formal proofs as easy as possible. C, C++ and Java are not. Languages like Java and (sometimes) C++ have too much possibilities so the proof is hardly possible in many cases. The limited functionality of the language is good for this purpose as it limits the number of possibilities one has to consider during the proof.
Also, if we want to program in Ada, which mcu development environment allow Ada programming? (I am not talking about compiling my own gcc tool-chain with ada enable)
Sorry, the only Ada toolchain I know is exactly that gcc. Its Ada compiler, gnat, is the one used by the Pentagon.
Home
Help
Search
Login
Register
