Writing correct code, part 2: bound functions (binary search part 4b)

Following on from yesterday’s article on invariants, this time we’ll talk about a second tool in the kit for thinking about code.  This one will be much shorter, because the Concept Of The Day is so simple.  It gets talked about even less than invariants, but let’s change that!

(Oh, and today is vegetarian-friendly Cheese Day at The Reinvigorated Programmer, though it still may not be much use to the vegans among you.)

What is a bound function?

You’ll remember that last time I said: “if your invariant properly expresses the intent of the algorithm, and if your code properly maintains the invariant, then that is enough for you to be confident that the code, if it terminates, yields the correct answer.”  The bound function is what tells you that the code does indeed terminate.

The bound function of a loop is defined as an upper bound on the number of iterations still to perform.  More generally, you can think of it as an expression whose value decreases monotonically as the loop progresses.  When it reaches zero (or drops below), you exit the loop.

The value of this concept is that it gives you confidence that the loop will exit. For this to be the case, you need only convince yourself (A) that the initial value of the bound function is finite, (B) that the value decreases by at least one on each iteration, and (C) that the loop exits when the value reaches zero.  But if there is a code-path within your loop that lets the value stay the same from one iteration to the next, then you might have an infinite loop.

What is the bound function for binary search?

As with invariants, choosing a bound function is something of an art; or let us rather say a craft, as it can be learned by experience.  For binary search, the obvious bound function is the size of the range that (our invariant tells us) must contain the sought value, if it’s anywhere in the array.

The exact representation of the bound function of course depends on how you represent the range.  Recall from last time that I opted to use a pair of integer variables, lower and upper, which represent the lowest and highest indexes into a[] that might contain the value.  With this representation, the bound function is upper-lower+1, because when the two indexes are equal you still have one more iteration to do.  (If you use a half-open range instead, with upper pointing one element beyond the last that could contain the value, then you get a nicer bound function of upper-lower.)

Notice that our bound function doesn’t necessarily tell us how many iterations we have to do — as noted above it’s just an upper bound on the number of iterations.  In this case, the bound function shrinks much more quickly than linearly.

Avoiding the inifinite loop in your binary search

Let’s take another look at the code that I claimed, last time, was perfect:

int binary_search(const int a[], const int size, const int val) {
    int lower = 0;
    int upper = size-1;

    /* invariant: if a[i]==val for any i, then lower <= i <= upper */
    /* bound function: upper-lower+1 */
    while (lower <= upper) {
        int i = lower + (upper-lower)/2;
        if (val == a[i]) {
            return i;
        } else if (val < a[i]) {
            upper = i-1;
        } else { /* val > a[i] */
            lower = i+1;
        }
    }
    return -1;
}

(This is identical to the version in the previous article except for the addition of the single-line comment specifying the bound function.)

So let’s informally verify, by means of the bound function, that the code terminates:

  • The bound function gets a perfectly good value at loop entry: lower is initialised to 0 and upper to size-1, so upper-lower+1 = size-1-0+1 = size.
  • Each time through the loop, i is set to a value no less than lower and no greaters than upper.
  • The first branch of the IF statement (val == a[i]) returns from the function, so we know that the loop exits if this condition is fulfilled.
  • The second branch (val < a[i]) results in upper being set to i-1.  But we know that i was not greater than upper, so upper‘s new value of i-1 must be strictly less than its old value.  Therefore the value of the bound function, upper-lower+1, is reduced by at least one.
  • By analogous reasoning, the third branch sets lower to a value strictly greater than its previous value, so again the bound function is reduced.
  • So on the exit from the three-way IF, either we have returned from the function or reduced the value of the bound function by at least 1.
  • Therefore, consecutive iterations either result in returning (when val == a[i]) or in progressively reducing the value of the bound function.
  • Finally, when the bound function’s value reaches zero or less, upper-lower+1 <= 0, which means that upper+1 <= lower, so upper < lower.  In other words, the condition guarding the while (lower <= upper) loop is no longer true, so the loop exits.

As with the walk-through of the invariant last time, this is much more detailed than you would usually do for real code — at least, for code as straightforward as a binary search.  Again, as with that code, it takes much, much longer to explain that to actually do.  Anyway, I hope that’s useful, and that having the notion of a bound function in your mental toolkit makes it easier to correctly develop subtle code.

Of course invariants and bound functions go very much hand in hand — in practice, you wouldn’t think about one without the other, and then bring the other to the party after the event (as I have done in these two articles): you’d choose both together, as both model aspects of the algorithm you’re implementing; and you’d have both in mind as you wrote the branches of the three-way IF statement.

So remember: the invariant helps you show that if a loop terminates, it does so correctly; and the bound function helps you show that the loop does in fact terminate.

But wait!, I hear you cry — the loop may terminate, and it may preserve the invariant as it runs, but what if the array wasn’t sorted to begin with?  Or what if the array pointer was junk, and pointed into the middle of a string instead?  And how does the caller of our binary search function know what the return value means?

The answers to these questions are found in preconditions and postconditions; and they will be the subject of the next (and probably last) article in this Writing Correct Code series.  Stay tuned!

Appendix: going deeper

In response to part 1 on invariants, superCat asked: “What’s a good book, language, environment, etc to be able to learn this properly“?

That’s an interesting question. The classic answer would be something like Dijkstra’s A Discipline of Programming [amazon.comamazon.co.uk] or David Gries’s The Science of Programming [amazon.com, amazon.co.uk].  But books that treat this kind of code-contemplation tool as a subject in its own right tend to be, frankly, rather boring. I know at least one excellent programmer who was so turned off invariants and suchlike by having to study them in detail that now he avoids the techniques completely, which I think is a real loss.  (That’s why his binary search routine was longer than it needed to be!)  So, anyway, an academic book is probably not the way to go.

If you want a deeper understanding than my article can give while still remaining firmly in the real world, then Bentley’s Programming Pearls [amazon.com, amazon.co.uk] may still be the best bet: it talks about many other things, too, but does place the concept of program proof firmly in the context of problems that we need to solve in real life; it makes proof a tool rather than an end in itself.

In the comments to the earlier article, Malcolm Sharman recommended How to Think About Algorithms [amazon.com, amazon.co.uk] by Jeff Edmonds.  I’ve not seen this myself, so I can’t second the recommendation, but the Amazon overviews look good.

I’d be happy to hear other recommendations.

About these ads

42 responses to “Writing correct code, part 2: bound functions (binary search part 4b)

  1. I love the series. It’s really made me think more about my algorithms.

    Also, I always enjoy the pictures of food…

  2. Good series of posts. One suggestion: when these posts are done, present a new problem for people to solve, using the techniques you’ve described.

  3. Phillip Howell

    I really would love to hear an explanation of why you chose an iterative solution for this problem; is it specifically so that you could discuss loop invariants and bound functions?

    Using iteration in this case causes you to have to think about the problem more than is necessary: in the recursive case there are four elements to think about (base case, method of descent, pre and post), but the iterative solution adds the loop invariant (substituting bound function for base case) — which is guaranteed by the pre/post in the recursive solution.

    Frankly, the loop invariant is the most complicated piece of thought in the iterative solution to this algorithm, and so being able to ignore it — by choosing a different solution — is pretty nice.

    What I’m really saying is: everything you’re talking about is implementation detail, and it feels a little bit like you’re missing a more important “big picture” question of how to start choosing a solution path.

    If it’s a pedagogical decision, that’s cool — but if you want to be complete or persuasive you should really address the issue.

  4. Jeshua Smith

    @Phillip – For what it’s worth, there were a number of people in my programming classes at college who understood iterative loops but couldn’t grasp recursion.

  5. Sjur Karevoll

    A very closely related concept is that of structural recursion. I’m a functional programmer at heart, so I often think in functions; every loop I write is envisioned as a recursive lambda. To make sure it terminates, it has to be structurally recursive.

    What this means is that for the function to be allowed to call itself, at least one argument has to be structurally decreasing. By structure I mean data structure, and by decreasing I mean less of it; lists must be shorter, trees can only recurse on their branches and stacks must be popped. Numbers have a trivial mapping to peano numerals, which again have a trivial mapping to singly linked lists with no data, so smaller numbers are structurally decreasing as well.

    Very often this is simple to prove; you’re actually recursing (or looping) over a data structure, and it is actually decreasing in size each time around. Other times you have to do a mapping, for example for numbers, which usually isn’t hard to do either.

    For example, in my binary search code (not posted), I used, as you did, a (lowest, highest) pair to represent the range of numbers. To prove to myself that this was structurally recursive, I provided a mapping to a (start, length) pair, `(lowest, highest) |-> (lowest, highest – lowest)`, and proved that the length was always decreasing, and that in the case that it was zero I would not recurse.

    I’m not unfamiliar with bound functions, but to me at least, thinking about structural recursion is easier: I can work with the structures I already have, or if I have to map it to something it doesn’t have to be a number.

    Unrelated: Beef and cheese may be pretty, but i find sushi to be even more aesthetically pleasing. Please don’t give them up altogether.

  6. Jason, you have correctly anticipated my intentions :-)

  7. Phillip Howell

    @Jeshua

    This is going to sound harsh, but: people who can’t grasp recursion should seriously think about looking for a different line of work. (Or go read _Godel, Escher, Bach_ until it sinks in.)

    Can you be an effective programmer without understanding it? Probably. But it’s a serious contraindicator.

  8. Phillip, I can’t really disagree with you that people who don’t understand recursion at all really don’t belong in a programming job.

    On the other hand, I am not as in love with it as you are. I spent some time trying to think of good rebuttals to your claim that “using iteration in this case causes you to have to think about the problem more than is necessary” and I’ve come to the conclusion that I don’t have to. Bottom line is, I just disagree. It’s as though you’d said “eating pizza in this case causes you to encounter more pleasant flavours than eating sushi”, and it just isn’t true for me.

    The way I see binary search, it is perfectly naturally expressed as an iterative algorithm: you start with a wide search space and you go round and round cutting it in half. Recursion feels less natural to me for this. It’s not like quicksort, where the very nature of the algorithm is recursive.

  9. Sjur Karevoll

    Once you’ve programmed enough in different languages and paradigms, you don’t notice the difference between recursion and iteration any longer.

  10. “Once you’ve programmed enough in different languages and paradigms, you don’t notice the difference between recursion and iteration any longer.” Sorry, that is [tries to think of polite way to write “complete nonsense”.] There are plenty of algorithms — we just mentioned quicksort, for example — that just don’t make any sense interatively.

  11. Phillip Howell

    @Mike

    Well, obviosuly the sushi is going to contain more pleasant flavors. But to point…

    It’s not that I’m in love with recursion; it’s a right-tool-for-the-job question. I suppose I’m biased toward recursion here because any time I’ve seen a formulaic definition of binary search, it’s been a recursive one, and the algorithm itself describes a tree.

    I’ll concede that this is possibly a flavor issue, but I’m not entirely convinced.

    @Sjur

    This might be true for you. I don’t believe it is true for me; if it is, the value of ‘enough’ is exceedingly high.

  12. Sjur Karevoll

    @Mike and Phillip

    I should perhaps qualify recursion by prepending tail: “[..]You don’t notice the difference between tail recursion and iteration[..]”

    More complicated recursions aren’t quite as natural, but once I’ve compiled them down to thoughtcode they start to look the same.

    I just tried writing quicksort iteratively and it wasn’t any harder than writing it recursively (which I did right afterwards). Indeed, the algorithm I had in mind was the same, but the iterative version required some stack management and flow control that was rather annoying and horrible but brainlessly mechanical.

    This is a rather tangential debate though.

  13. /There are plenty of algorithms — we just mentioned quicksort, for example — that just don’t make any sense interatively./ -Mike

    If you don’t have a natural feeling for queues then quicksort or flood fill may seem unnatural as iteration. but someday you’ll be working in a language without proper support for recursion — e.g. Java, C++, Ruby. Then you’ll quickly discover that flood fill will destroy your stack. Quicksort is unlikely to do so, but it could someday.

    You will have to emulate tail calls with trampolines (Java is too broken even for that) or you’ll have to find queuing natural. And it really is natural once you get used to it. Iteration and recursion are the same thing; it’s just the language idiom that makes them seem different on the surface.

  14. /there were a number of people in my programming classes at college who understood iterative loops but couldn’t grasp recursion/

    Joel Spolsky wrote once on his long-lost and abandoned blog that the two key tests of whether a person could think like a programmer were recursion and pointers. If someone came quickly to a natural and competent understanding of either one, he had programmer nature somewhere in his soul.

    An understanding of iteration, on the other hand, doesn’t really indicate anything.

    I don’t necessarily think that conclusion disagrees with what I posted about recursion and iteration above.

  15. For quicksort to destroy my stack I’d need to be sorting enough elements that log2(n) stack frames weren’t possible. I don’t know of any modern language that won’t let you have a thousand stack frames, which means quicksort is good for problems up to 2^1000 =~ 1.07 million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million million elements.

    I am not going to lose sleep over that.

  16. I don’t know if I’d call quicksort naturally recursive. It’s naturally stack-based, and recursion is a simple way of implementing a stack, but I can’t see any fundamental difference between storing data in an explicit stack or in the function call stack.

  17. From the comments I’ve seen in these past few posts, I don’t believe I’ve seen solution that returns the “If the value was present, it would have been here” location. Say, the negative index of where it would have been, had the element been present.

    Possibly I’m just spoiled by the JDK binary search algorithm…

  18. Simple recursion and iteration are the same beast with different collars. The invariant is just the precondition of the recursive function and the bounding function is needed to demonstrate that you can apply induction from the base case to the recursive ones.

  19. Arild Haugstad

    Given a naive implementation of quicksort, it may easily overflow the stack on “worst case” input:
    A “natural” recursive implementation will make a recursive call for each subsequence to be sorted.
    Unless the compiler optimises tail calls, that means a stack frame for each call — and even if it does, unless the programmer takes care, it’ll probably save the recursive calls on either the “bigger than” or the “smaller than” side of the pivot, rather than ensuring that the call is saved on the side with the most elements.
    The worst case is when, each time, one of the subsequences are empty. (*And* we haven’t done something clever like *not* making a recursive call on subsequence with the most elements.) In that case, we make “n” calls when sorting “n” elements…

    Depending on how the pivot is chosen, the worst case input may seem extremely unlikely — unless someone is *trying* to break the software, or the method is something incredible naive, like “select the first element”. (“Select the first element” *was* the method presented in my undergraduate algorithms textbook…)

  20. I’m with Phillip Howell in thinking that recursion is by far more natural for this problem.

    But then, I just finished writing a book on Clojure. So I might be biased.

    Formally, iteration and recursion are equivalent. To me, what really brought this home was when I became completely comfortable with the loop/recur construct in Clojure. Is it a loop? Is it recursion? The ideas really start to become blurred. I find my mind keeps flipping back and forth between the representations, like it does with the Duck Rabbit (http://commons.wikimedia.org/wiki/File:Duck-Rabbit_illusion.jpg). The more it flips, the easier it is to see that recursion and iteration are two sides of the same coin.

    Now, I’m a big fan of immutability, so I think I’ll always prefer recursion for that reason, since it’s conceptual model doesn’t demand thinking about “changing” variables. But I can see how the inherent complexity of the problem is the same. Loop invariants are are similar to the concept of “what a function does”. Pre and post conditions are encoded in the arguments and return value of a function. Bound functions are similar to the concept of making progress towards a base case in a recursive function.

    I agree with Phillip that this vocabulary seems strange and unnecessary for a fan of recursion. But then, discussions of base cases and (for other examples) aggregator arguments probably seem superfluous for someone more used to iteration.

    I’d say: know both, be at least capable of writing any algorithm as either, but feel free to have a favorite.

  21. Luke V. wrote:

    Loop invariants are are similar to the concept of “what a function does”. Pre and post conditions are encoded in the arguments and return value of a function. Bound functions are similar to the concept of making progress towards a base case in a recursive function.

    Dude! Stop pre-empting my future articles!

    :-)

  22. Phillip Howell

    Recursion and iteration are equivalent similarly to the way that Perl and C are equivalent. Perl and C are both Turing complete, but I’m not not going to write systems in Perl or text processing scripts in C.

  23. What Phillip Howell just said.

    (This, too, was slated to the subject of a forthcoming article … If only I had less perceptive commenters, I wouldn’t keep getting scooped. Seriously, though, people, keep it up — it’s great.)

  24. Well, yes. But I think merely arguing “recursion vs iteration” is too naive – which one is simpler or more idiomatic depends entirely on the language in question and the programming paradigm you’re using.

    If I’m using Haskell or Clojure, it would probably never even occur to me to use iteration. If I’m writing in Assembler, or a language that doesn’t support tail optimization, I’ll definitely tend to reach for iteration first.

    And half the time, in a really good language, you don’t do either, and use list comprehensions, higher-order functions, or pattern matching instead.

  25. Phillip Howell

    @Luke

    Absolutely. You have to know what tools are in your toolbox and use them appropriately. Sometimes you’re free to choose a language / paradigm that suits the problem; sometimes those choices have been made for you — the set of tools you have at your disposal is thus narrower.

    There’s no One True Way to do anything. Just the right way to do something for a given context.

  26. Pingback: Binärsortering « Åke i exil

  27. Scott O'Dell

    Mike, thanks for writing these articles. I can imagine it’s hard to publish code for such a tough audience.

    Maybe it’s just because I’ve been programming for underpowered embedded systems, but although lately I’ve programmed recursively in LISP, your code has a strong argument for being more efficient. Even with optimized tail recursion, the function parameters still have to be bound to the new lexical scope for every function call when using a functional style. It’s not a big deal for logarithmic explosive searches, but for exponentially explosive functions, an iterative method may be significantly faster.

  28. @Mike Taylor

    Regarding recursion vs. iteration. The kernel mode stack is between one and three pages depending on Operating System. That is 4-12kB on x86. Recursion is usually banned in kernel mode code.

    This doesn’t mean recursion is “bad” (i’m a fan of functional languages…) but it means there are cases where iteration is the only option.

    Also, it seems to be a matter of taste. You say that you find iterative binsearch and recursive quicksort “natural”. I find the opposite to be true in my case. I find recursive binsearch and iterative quicksort to be “natural”.

  29. For anyone looking for books: ‘Error Free Software: Know-How and Know-Why of Program Correctness’ by Robert Laurence Baber (part of the Wiley Series in Software Engineering Practice) is a pragmatically-oriented starting point.

  30. Really appreciate these posts, I’ve bookmarked them all for more in depth reading of the discussion in the comments, at least the ones that weren’t by certain snarky vegans! I laughed at the cheese note.

    But seriously, thanks for this series, keep it up, please!

  31. Paul Winkler

    Nitpick (completely irrelevant to the main thrust of the article): Why do people keep writing “lower + (upper-lower)/2″ instead of “(lower + upper)/2″?

    They’re equivalent, but I like the shorter version.

    There’s a marginal speed improvement too, although I would guess that for most input, a single extra subtraction in the inner loop isn’t going to bother anybody.

  32. Probably bug number one of Binary Search: Overflow.

  33. Actually, I think people have gone way overboard on the significance of the overflow “bug” — not here, particularly, but in general. I certainly can’t think of any time I’ve needed to binary-search more than two billion items, and I think that characterising (lower+upper)/2 as a bug is extremely harsh. Still, since it’s a known issue, and since it can be easily addressed (gaining one more bit of supported array-size) it seems as easy to use the safer version as not.

  34. Pingback: Writing correct code, part 3: preconditions and postconditions (binary search part 4c) « The Reinvigorated Programmer

  35. @Scott O’Dell

    Your comment is closest to my thinking on this issue. Stack overflow or no, the additional overhead on method calls in many (most?) languages is going to make an iterative algorithm faster.

    In school, I was taught to “think recursively, write iteratively,” and sometimes to write recursively as an intermediate step. Being able to change a recursive algorithm into its iterative form (and vice-versa) is the important skill here. It helps me prove to myself that I understand the algorithm, and gives me a second perspective from which to look at the problem, helping me to write clearly and correctly the first time.

  36. Paul Winkler

    I guess it’s been too long since I used a language where ints CAN overflow ;)

    Hmm. I’m trying to think of a more explicit way to write the non-overflow version. It’s clear on reflection how it avoids overflow, but it doesn’t exactly announce its intent. Maybe it does if you write a lot of C.

  37. Pingback: Another challenge: can you write a correct selection sort? « The Reinvigorated Programmer

  38. Pingback: What does it take to test a sorting routine? « The Reinvigorated Programmer

  39. For books, my Theory of Algorithms class used “Algorithm Design” [1]. It’s predictably dry, but it’s easily one of the best textbooks I’ve encountered. Not only does it show the correct results, like every other book, it shows *incorrect* results, and *why* they’re wrong, and *why* people fall into incorrect approaches to the problem. It also proves everything it uses, so the book itself is internally consistent and effectively contains everything you would need.

    [1] : http://www.amazon.com/dp/0321295358/?tag=hashemian-20

  40. Pingback: Programming Books, part 5: Programming Pearls | The Reinvigorated Programmer

  41. This is an excellent series. I have been like many other programmers who simply -1 from the loop condition to coup with the outofBound Error, which is error-prone and a waste of our human brain. This series saves me!

  42. Thanks, zsjulius! It’s really encouraging that this two-and-a-half-year-old post is still finding readers.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s