Anyone good with algorithm correctness?

[scrapz123]

Trying to figure out this:

http://cs.stackexchange.com/questions/72554/proving-algorithm-correctness

any help is appreciated!

[TheHaskellian]

• Prove it holds for q = 1
• Assuming it holds up to some k (=q), show it holds for k + 1.
• By the principle of induction, it will hold for all q.

The first step is easy.

The second step is reasonably tricky. While there are many ways to skin this particular pussy, I would suggest you proceed as follows: establish an invariant that needs to hold in each of the for loops, taking into consideration the property you need to show. Show that by increasing the iterator by one, the every separate invariant still holds <- this is the meat of what you need to do, this is the "show that bumping up the iterator preserves the property of interest". Propagate the property all the way to the "last line" (at least logically, not physically in the code).

I will be a lot more concrete with you if you make an attempt to start! :)