CODEWITHSUNDEEP
computer-scienceproofcorrectnessproof-of-correctness
Becky L
Becky L

Reputation: 31

Proving the correctness of a program

The function recursively finds and returns the smallest element from a array that has integer elements

Min(A, b, e)
if (b=e)
     return A[b]
m = (b+e)/2 // floor is taken
x = Min(A, b, m)
y = Min(A, m +1, e)
If(x < y)
     return x
else
     return y

My precondition is: b and e are integers greater than zero

My post condition is: return a integer either x or y (not sure about this)

So how can I prove this is correct by showing that the pre and post condition are inductive

Sorry for the format, new at this.

Upvotes: 2

Views: 820

Answers (1)

Patrick87
Patrick87

Reputation: 28292

Proof: the proof is by mathematical induction.

Base case: consider the case where b=e. We are looking at a portion of the list A with size 1; the minimum element of a list with one element is the list's one element, which the algorithm returns in this case.

Induction hypothesis: Now assume that the algorithm correctly returns the minimum element for all lists of size up to and including k. To prove: it returns the minimum value for lists up to size k+1.

Induction step: We have e = b + k + 1 and want to show that we return the minimum element. We know that m will be equal to (e+b)/2 = (2b+k+1)/2 = b+(k+1)/2. This will divide the list of size k+1 into two parts of size floor((k+1)/2) and cieling((k+1)/2). Both of these are less than or equal to k for all values of k greater than zero (our base case starts at k=1, so this mean's we're good). Thus, by the induction hypothesis, x is the minimum value of the lower half of the list, and y is the minimum value of the upper half of the list. The algorithm returns x if it is less than y, and y otherwise. Since the minimum value in the list A must occur in one half of the list, and we return the lesser of the minimal values from the two halves of A, we know we're returning the minimal value in A. This concludes the proof.

Upvotes: 1

Related Questions