Program Correctness - Termination

The way we have gone about proving termination was a little interesting since we have used the principle of well ordering. I've never thought we would actually use this and it definitely helps in my understanding of well -ordering since at first I couldn't really think of a nice example where well-ordering is absolutely clear and makes intuitive sense. For example proving termination of an iterative binary search program meant that we had to show the difference between the last element's index and the first element's index in the array/sub-array was a decreasing finite set and so it must have a smallest element. Indeed it is true that when F >= L can only happen if F = L happens first since either F or L changes in each loop iteration decreasing by 1 (never both changing). And so F = L implies L - F = 0 where 0 is the smallest element in a natural numbers set. And we know L - F is always decreasing by one as was shown in lecture so that Li+1 - Fi+1 < Li - Fi where i is the ith iteration of the loop assuming i + 1 iterations happen (in other words either F or L decrease by one in each iteration and so L - F continually decreases). So since Li -Fi is a decreasing sequence of natural numbers (since L and F were natural numbers and decreasing either by 1 each iteration keeps them as natural numbers) then it must have the smallest element 0 and so the loop will terminate. It's neat to see induction playing a role in everything we are doing now and seeing this it seems to be a very fundamental computer science concept. I guess we'll be seeing again in 263!