> If the current comparision shows a smaller value, we update smallestSoFar.<p><pre><code> if ( a[smallestSoFar] > a[nextToCheck] ) {
</code></pre>
This code makes me twitch. Finding a smaller value by checking to see if the old value is larger than the new value... Instead of checking to see if the new value is smaller than the old value.<p>Additionally, calling the value you are <i>currently</i> checking 'nextToCheck' is also confusing. It's not the next one, it's the current one.
One of the things I find funny is that the halting problem is the least of my concerns working in mainstream programming languages today.<p>Maybe back in the day when people were using basic and assembly language it was easy to write some gawdawful mess but since structured programming I think it is easier to do the right thing rather than the wrong thing. Partially because we have good constructs to work with, secondly they are good constructs to reason with -- for instance, you might have the idea of a loop invariant in your head when you write the loop, even if you don't call it that.
Hey, this seems like an application of induction. You choose some property you want to prove about your program, show it is true before the loop (base case), then show it remains true for any next iteration (inductive step), therefore it is true for all iterations.<p>It reminds me of the hand-wavy inductive proofs I run through my head when I write recursive functions. Usually it's not even about eliminating bugs, it's just the most natural way to understand why the code works. It seems less natural for imperative for/while loops but still a good tool to keep in mind.
As a source of motivation for students, does anyone could point me to some "real (open source) code" where the programmer commented a loop with an invariant for clarity.
If I made a zeno's paradox loop:<p><pre><code> bigFloat delta = 0.5
bigFloat total = 0.0
while total < 1.0:
total+=delta
delta*=0.5
</code></pre>
Where does this fit in the model of using a loop invariant to show the loop terminates?
The loop is always approaching the terminal case (and eventually the machine runs out of memory)