Writing correct code, part 1: invariants (binary search part 4a)

I’m struggling with my article numbering now :-)

Regular readers will have noticed that I am running a whole bunch of series in parallel on this blog: one reviewing programming books, one on the issue of simplicity in programming, one reviewing Series 5 of Doctor Who, a related one on Russell T. Davies’s contributions, and one on learning Lisp.  To my huge surprise, what started out as a review of Jon Bentley’s book Programming Pearls [amazon.com, amazon.co.uk] has led through a sequence of digressions and become a series of its own on binary search.  This is part 4 of that series: when I’ve finished part 4, I will — at last! — progress to the actual review.  But since part 4 is about the distinctly non-trivial subject of writing correct code, it will itself have to be composed of multiple sub-parts.  So this article on invariants is both part 1 of the new writing-correct-code series and part 4a of the binary-search series.  Hope that’s clear.

A few people have complained about the sushi pictures on this blog, so before I plough into the article proper, here is something completely different.

Tools for thinking about code

In previous articles, I’ve complained about using testing as a crutch (note: not complained about testing), and rather self-righteously claimed that people should think about their code.  What exactly do I mean by that?  In this mini-series, I want to draw attention to a few concepts that will be patronisingly familiar to most of you who have CS degrees, but which will hopefully be helpful to any avocational programmers hoping to tighten up their code.  Anyone who attempted the binary-search challenge and didn’t get it right first time (modulo syntax errors and other such trivia) might find something of use here.

The three tools I have in mind are:

  • Invariants
  • Bound functions
  • Preconditions/postconditions

These are powerful concepts, and can be used at different degrees of formality and rigour.  At one extreme, some computer-science researchers might try to use these concepts to mathematically prove the correctness of a piece of code — perhaps with the proof being an order of magnitude longer than the code.  At the other extreme, a seasoned professional developer probably always has at least a fuzzy and informal notion of an invariant in the back of his head whenever he writes a loop.  I think that we would often benefit from thinking more explicitly about invariants.  But note that in this article I will go rather overboard for the purposes of explanation, and use a level of detail that I would never normally use for a program as trivial as a binary search.  So: I am not suggesting that we should invest this level of analysis in every loop we ever write.

What is an invariant?

An invariant is a property that remains true throughout the execution of a piece of code.  It’s a statement about the state of a program — primarily the values of variables — that is not allowed to become false.  (If it does become false, then the code is wrong.)  Choosing the correct invariant — one that properly expresses the intent of an algorithm — is a key part of the design of code (as opposed to the design of APIs); and ensuring that the invariant remains true is a key part of the actual coding.  Roughly speaking, 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.  (Ensuring that it does in fact terminate is the job of the bound function, which I will talk about next time.)

As usual, an ounce of example is worth a ton of explanation, so let’s go back to the problem of binary search, and see if we can build a routine whose correctness we’re confident of even before we run our tests.

A brief recap of linear and binary search

Here’s a quick reminder of what binary search is about.  The goal is to find a value in an array.  If the array contains one or  more instances of the value, then the search function should return one of the indexes of the sought value, otherwise it should return -1.  (To help us concentrate on the algorithm, we’ll assume that the values are all integers — we could do this with templates and generics and whatnot, but for our current purposes that would only obscure the algorithmic issues that we want to concentrate on.)

In the general case of searching in an array, you can’t do better than the trivial linear search code (expressed in C; the code is pretty much identical in C++ or Java).  Here we call the array a, it has size elements, and the sought value is called val:

int linear_search(const int a[], const int size, const int val) {
int i;
for (i = 0; i < size; i++)
if (a[i] == val)
return i;
return -1;
}

This function takes, on average, size/2 probes to find an element that is present, and size probes to determine that one is absent.  We say that it is O(n), which means simply that its run-time is proportional to n.

But if we are allowed to assume that the array is sorted (in ascending order) then we can do much better.  We can use the binary search algorithm: here, we cut the search space in half at each step rather than reducing it by one.  We guess that the middle element of the array might be equal to val; if it is, we’re done, otherwise we can narrow the search to either the top half of the array (if the mid-point is less than val) or the bottom half (otherwise).  Then we probe the midpoint of the new, smaller, range, and continue in this fashion until we either find the element or discover that the remaining range is empty.

Because binary search cuts the search-space in half at each step, it converges on the desired value much more quickly than linear search — in log2(n) steps.  For very small arrays that difference is negligible; but when searching in an array of a million elements, binary search needs 20 probes rather than 500,000 on average for a linear search.

What is the invariant for binary search?

In informal terms, the invariant for this algorithm is: “if the sought value is present in the array at all, then it is present in the current range”.

To make it useful for deriving correct code, though, we need to formalise that invariant in terms of specific variables and values.  And before we can do this, we need to decide on the representation of the range under consideration.  There are several candidate representations, none of them greatly better or worse than the others: we could keep track of the highest and lowest array indexes that might hold val, or the lowest index and the size of the range; or use asymmetric indexes, where we maintain the index to the base of the current range and the index that points past the end.  For this version of the routine, I’m going to arbitrarily choose to represent the range by two variables, lower and upper, which contain the lowest and highest indexes into a that might contain val.  With this representation, we can formalise the invariant as:

if val is at any position i in a, (i.e. a[i]==val) then  lower <= i <= upper.

So long as we ensure this invariant is kept true, we can be confident that our code will not fail to find val if it’s present.  (This doesn’t show that the program will terminate, but we’ll look at that next time.)

Armed with this invariant, we can write the code with some confidence that it’s right (and indeed this C function that I just wrote passed all tests first time):

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 */
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;
}

Informal proof of the code

Here is the reasoning that led to the code above, expressed pretty informally.

  • The first thing to do is establish the invariant that’s going to hold true for the rest of the function, so we set the variables lower and upper to appropriate values (i.e. the lowest and highest indexes within the whole of a).
  • We have ensured that the invariant is true when we first enter the loop.  To show that stays true throughout the running of the function, we need to show that whenever it’s true at the top of the loop, it’s also true at the bottom.
  • The first statement of the loop (assigning to i) does not affect any of the variables referenced by the invariant, so it can’t possibly cause the invariant to stop being true.  (Note that a and val can never be changed as we declared them const, so we only need to worry about lower and upper.)
  • What follows is a three-way IF statement: we need to show that each of the three branches maintains the invariant.
  • The first branch covers the case where we have found the sought element.  At this point, we’re returning from the function (and therefore breaking out of the loop) so we don’t really care about the invariant any more; but for what it’s worth, it remains true, as we don’t change the values of lower or upper.
  • The second branch (val < a[i]) is the first time we need to use non-trivial reasoning.  If we’re in this branch, we know that the condition guarding it was true, i.e. val < a[i].  But because a is sorted, we also know that for all j > i, a[j] >= a[i].  This means that val < all a[j] with j >= i, so the highest position it can be at is a[i-1].  Knowing this, we can set upper to i-1, and know that the invariant still holds good with the new, more restrictive value of upper.   Notice what has happened here: we have shrunk the range to half its previous size or less, but simple reasoning about the code persuades us that we still know where val must be (if it’s anywhere in a).  We are confident that we have not inadvertently excluded it from the range.
  • The third branch follows the same form as the second: since we know that val > a[i] and that a[i] >= a[j] for all j < i, we can conclude that the lowest position val can be at is a[i+1], so we adjust lower accordingly and maintain the invariant.
  • Since we’ve verified that all three branches of the IF maintain the invariant, we know that the invariant holds on exiting that IF.
  • That means the invariant is true at the bottom of the loop, which means it will be true at the start of the next time around the loop.
  • And by induction we deduce that it always remains true.
  • Finally, we break out of the loop when the candidate range is empty, i.e. when it’s been shrunk to negative size, so lower > upper.  At this point, we know that the condition of the invariant (“if val is at any position i in a”) does not hold, so the invariant is trivially true; and we return the out-of-band value -1.

Does this sound like an awful lot of work?  When it’s spelled out step by step in this way, yes; but in practice, you never need to go this slowly and carefully unless you’re writing avionics software, a life-support system’s firmware, or a Reinvigorated Programmer article.  The point is not necessarily to go through the code in small pedantic steps like this, but to spend some time up front understand what the invariant is, keep that invariant in mind while coding, and understand the resulting code to whatever depth seems appropriate.

It takes much longer to read about this (and much longer to write about it!) than it does to actually do it.  Writing the C function above took two or three minutes; just being explicitly aware of the invariant was nine tenths of the battle.

This code is good

I’m going to claim that this code is objectively better than most of the solutions that were posted in response to the original challenge — better, even, than most of the correct solutions.  [Yes, I realise that I am setting myself up for a really big fall if someone finds a bug in it!]  Here’s why:

  • It’s short, which makes it easier to understand and maintain.
  • It has no special cases — array of length 0 and 1 are handled by the main code.
  • The single comment is genuinely informative.

In short, the code obeys the golden rule from The Elements of Programming Style: “Say what you mean simply and directly“.

Through the use of a simple but powerful technique, I was able to write compact, clear code in a short time; and be pretty confident, even before I tested it, that it was correct.

That last point is important not as some kind of macho posturing, but because it means that the tests, when I run them, are giving a second distinct line of sight on the problem.  I’m not using tests to make my code right (even if that were possible, which I’ve argued is not the case).  Instead, I have written code that I already think is right, and I’m using the tests as an independent line of verification.  You may remember in the last post that I said: “writing tests lets you triangulate”; I was trying to be conciliatory towards all the test-driven developers out there, but actually that’s not true most of the time — because if the tests are the development then all you’re getting when you run them is validation that doing the same thing again gives you the same result.

Let me try an analogy to explain what I mean.  If I am paying the bill at a restaurant and I want to add up the amounts for the various dishes, I add from top to bottom, then verify by adding from bottom to top.  By approaching the same problem from two different directions, I give myself the best chance of avoiding mistakes; whereas if I add in the same direction both times, I am liable to repeat a “favourite mistake” like adding 8+7 and making the result 13 rather than 15.  Or I might verify by using another different technique such as column-at-a-time-and-carry.  The point is to use multiple techniques that have different points of weakness.

But when testing and development are the same thing, then I can’t use testing to verify my development.

Why does no-one talk about invariants?

The great mystery to me is why no-one seems to talks about invariants any more.  You will of course find them in The Elements of Programing Style, Programming Pearls, and other books of similar vintage, but they are not to be found in, say, Refactoring.

Here is an amazing statistic: the original binary-search challenge post has now attracted more than seven hundred comments.  Of those seven hundred, only three comments [Mihai, dave, Darius Bacon] so much as mention invariants.  (All three comments are candidate solutions to the binary-search challenge: Mihai’s and dave’s use invariant assertions and Darius’s mentions the invariant in comments.)  That is astonishing to me, given that we’ve all been trying to solve a problem that is known to be subtle — I warned about its deceptive difficulty up front — and one that is so amenable to analysis using an invariant.  I can only assume that they don’t teach invariants in CS degrees any more.  (Surely that’s not actually true?  Anyone graduated recently care to comment?)

Here is my best guess on how such a useful technique has become so unfashionable: I think it’s collateral damage from the huge popularity of object-oriented programming.  The ability to reason rigorously about a program depends on having solid knowledge of its relevant state, and what is an “object” but a big opaque ball of mutable state that can change under our feet?  Yes, objects “hide” state by encapsulating it; but it’s still there — everyone is naked under their clothes.  Changes to object state cause changes to its behaviour, which makes them hard to reason about.  (This is why object-oriented techniques don’t work well in concurrent systems, hence in part the growth of interest in functional languages as multi-core processors become increasingly ubiquitious.)

[Note well -- and I say this because almost everything I write on this blog seems to get misinterpreted somewhere or other: I am not, repeat not, saying object-orientation is A Bad Thing.  I am saying that it has a specific and important drawback which ought to be taken into account, alongside its benefits, when deciding where its use is appropriate.]

Finally, I think there is a practical point to be made here: where languages have facilities that let us mark objects as immutable, or mark methods as pure queries, we should take advantage of them whenever possible — as I did in the code above, where a, size and val were all marked const.  And where languages lack those features, we should grind our teeth in fruitless despair and cry out to the heavens.  (Although I love Ruby, I hate the fact that it has no way to talk about these things.)

There you have it: invariants!  They’re easy to use, very powerful, and let you think clearly about subtle code such that your program has a good chance of running right first time; and they provide a different axis of analysis that allows your tests to be more informative.  Get in the habit of using them!

About these ads

102 responses to “Writing correct code, part 1: invariants (binary search part 4a)

  1. So in the most common error of zero length array, how is your invariant true?

    Seems like people assumed too much strength in the invariant rather than the opposite view that you’re espousing here.

  2. Vorlath,

    The invariant is: “if the sought value is present in the array at all, then it is present in the current range”. When the array is zero length, the precondition is false. As you know, any statement of the form “if A then B” is equivalent to “not A or B”, and since not A is true, the invariant is trivially true for an zero-length array.

  3. Great article. Personally, having tried and failed I really see the benefit of having invariants. Though I have a question. How come the invariants change from (hi<=low) to (hi < low) if you use a recursive approach?

    PS. Bring back sushi. I love meat as much as the next guy but meat is not you.

  4. Daniel, I don’t think there is anything about a recursive solution, as opposed to an iterative one, that demands the loop condition (not the invariant) use < rather than <=. But as I discussed, there are several different weays of representing the range, and if you use asymmetric bounds (i.e. your top-end-of-the-range variables indicates the index one past the highest possible one that could contain val), then you would of course us a strict inequality.

  5. For the record, my solution asserted the invariant as well (the comment above the loop describes it, and the asserts inside enforce it).

    I’m studying CS (as a part-time student, planning to have it as a minor if I ever graduate; my day job is programming computers and I’m planning a major in pure math), and invariants are mentioned in required early courses but I haven’t seen them getting nearly the prominence they deserve compared to testing.

    Maybe it’s that I’m as much of a mathematician as a programmer, but I’ve found thinking in terms of the same things I’d formalize for a correctness proof (though rather less formally) makes it easier to handle problems ranging from stupid typos (“That’s not supposed to happen. What could cause it? Hmm… that comparison looks backwards”) to inadequate specification (“I need to know which of these holds, and the spec doesn’t tell me; time to clarify the spec”).

    (I need to, someday, add testing to the list of things I’m good enough at to do it naturally – better testing would have caught some bugs I spent a while scratching my head over. But I still think I’m a lot better off with good reasoning-about-code skills and poor testing that I would be the other way around.)

  6. If you feel invariants have gone away it’s probably because you don’t have to read the literature that talks about them. Invariants are still a research area in CS.

    Betrand Meyer writes about invariants in Object-Oriented Software Construction (which I’m told was a famous book at the time). The whole pre/post condition idea was started by Tony Hoare in his article An Axiomatic Basis for Computer Programming. Betrand made it more “objecty” and coined the phrase Design by Contract.

    .NET languages recently had quite sophisticated support for these contacts added http://research.microsoft.com/en-us/projects/contracts/ . Not quite in the Eiffel style but enough to allow people to start pulling out proofs.

    In a similar vein people like Dijkstra (who took the extreme view that all programs should come with proofs) and David Gries have argued for programming in a more rigorous and mathematical fashion.

    Writing good invariants is hard though.

  7. I’m in second year computer science (in Belgium) and invariants were taught extensively last year.

    Although I must admit I didn’t use one when attempting the challenge. In the end I didn’t fare too bad, my code just didn’t support 0 length arrays. (Note you can’t verify this statement as the comment system gobbled my code two times and I was too lazy to resubmit :) )

  8. Branden Rolston

    I’ll chime in to say I graduated with my CS degree in 2008 and I don’t remember invariants being mentioned in my coursework. I was ignorant of the concept before reading your post.

    It’s interesting then that my solution was, except for being in Python, identical to yours. But it took me about ten times longer to get there. I spent probably 20-30 minutes walking through cases in my head before I had a correct solution. (I didn’t post it because I’m lazy and/or a coward.) So it seems invariants are an inherent property of an algorithm. You can either reason about them directly or waste time until you stumble upon them.

  9. Fleeting comment before bed, but having just finished TAing “Programing Reasoning” to our first year undergraduates, I know that at least one university in the UK still teaches them, in decent depth. It’s a follow on course from their introductory logic, and covers strong and well founded induction, program proofs via invariants and an quazi-formal program proof calculus for both Haskell and Java. Then then have to prove properties of a lot of well known algorithms.

  10. “A few people have complained about the sushi pictures on this blog, so before I plough into the article proper, here is something completely different.”

    Meh. Not that different after all. It’s still food ( unrelated to code ) – and dead living beeing ontop of it. Those pictures set me off reading your posts before, and will in the future. Consider your vegetarian audience.

  11. What’s a good book, language, environment, etc to be able to learn this _properly_. I have read K&R, and that’s about it.

  12. Another small correction: my answer was another one with explicit invariants (and a contract and loop bounds). I guess it didn’t show up because my comments spelled ‘invariant’ as ‘Inv:’ and ‘precondition’ as ‘Pre:’ (I use this stuff enough to consider the abbrevs worthwhile.)

  13. I don’t think OO can be blamed for ignorance of program derivation, incidentally — it was in classic 80s books like _Abstraction and Specification in Program Development_ and _Object-Oriented Software Construction_. That part of the material didn’t catch on nearly as much, but it was there.

  14. Cornell University student here, just letting you know that the junior-level required course, “Functional Programming” spends a lot of time on invariants as a lead-in to partial correctness proofs, and you get points off for not testing for the invariant explicitly.

  15. Thank you, Mike.

  16. bey0ndy0nder

    We talked about invariants in school (grad. 2007) just don’t remember much about it in terms of programming projects. (I did do a lot of proofs of correctness through axiomatic semantics. Disclosure: I went a 3rd tier state university.) I know what it is, and I use it sometimes, especially when coding math stuff (invariants comes out of the equations.) But not nearly enough, I admit–that I don’t really think in terms of invariants. Maybe implicitly I think about it, though. Thanks for reminding me to use it more often, from now on I will make sure to use it often. (I do think in terms of contracts when I code.)

    This is surprising–not explicitly thinking about invariants–considering I also have a math degree. Maybe the adage jack-of-all-trades master-of-none is a good description of what I do. Ha.

  17. bey0ndy0nder

    Also, you bring up very good points about thinking *hard* before coding. It seems like most of the time I just think a little, then code, then test, rinse and repeat. I need to pay more heed to thinking.

    But I also tend to do this when I’m doing math proofs though–the not fully thinking things through thing. I usually sit there and go through papers till I get it. Maybe this is how I think. (Although I’ve gotten a lot better at gaining insights. Practice really makes perfect.)

  18. Mike,
    That’s a great explanation on invariants. I’m one of those programmers who has the vague notion of what must hold true whenever I had to write algorithms such as these, but looking at the nice clean algorithm, and the fact it took u only a few minutes to write up, really shows why defining invariants formally is valuable! It took me a good 20 minutes to come up with my algorithm, and most of that was spent desk-checking with boundary conditions. Looking at how easy it was to formally define the invariant, it would’ve saved me quite a bit of time!

    I’m one of those that believe a good test does not a good function make. If you pay more attention to your test code than your code, your tests will be better than your code, and you’ll take longer writing your code because of the debugging required. Tests are still useful to prove to yourself and others that code works under expected conditions, but they won’t help you write maintainable code.

    With ur O-O comments, I think there is a real trap for developers starting out (particularly in non-typed languages) in making objects mutable without good reason. Whenever I write a new object, I always default to making it immutable unless there’s a good reason to make it mutable (e.g. the object is an entity with a definite identity and lifecycle). You have to consider whether the object needs to change over time, and why it must change. If it doesn’t need to change, prevent it! I can’t stress enough that the hardest bugs to find in O-O code are due to unnecessary object mutability!

  19. Malcolm Sharman

    A book I quite enjoyed on this topic of invariants in algorithms is http://www.amazon.com/Think-About-Algorithms-Jeff-Edmonds/dp/0521614104/ref=sr_1_1?ie=UTF8&s=books&qid=1272262880&sr=8-1

    The diagrams are bit dodgy and crude, but the content was quite interesting. Made me think a lot more about how to put algorithms together from a starting point of invariants.

  20. Invariants and pre-/postconditions are still taught where I graduated from, not very formally though. Most professors would try and get the students acquainted with the the concepts, verify them in simple algorithms like finding the minimum element of an array or selection sort, but wouldn’t focus that much on them.

    They’re sort of implicit to me when I think about a problem. Sure, formal verification is a good thing, and it’s good to know your program works before other people put their trust on it. But I’ve never stopped to ask myself “Hey, what’s the loop invariant here?” – I guess I did when I was writing library functions and implementing containers, but with time I sort of in-formalized them in my head.

    They’re really useful though. Anything that helps me avoid “kludge-until-it-works” usually is. :-)

    PS. I laughed a lot at the meat images! ;)

  21. Don’t take any notice of the complaints. The pictures of sushi were fine to break up the text. :-)

  22. How would I be able to develop my programming skills like you all, what books, paradigms are reocommended to learn, I’ve only read K&R, and done some of the exercises.

    Any recommendations?

    Thanks mike for the wonderful blog, I read it each morning now :P

  23. I’ve taken two (first and second year) logic courses at UToronto this year, and in both we’ve studied invariants. Not nearly as hands on as in your example, however, which I’m sure is partly to blame, as through the thick vail of rigorous proofs students surely fail to see the applicability of the idea, dismissing it as just another “study the night before” course.

    Also I am vegetarian, and demand some tofu and bean based dishes to be represented to avoid culinary discrimination.

  24. Hollis Waite

    Personally, I think that a binary search should use negative return values to indicate where a missing element would be if it were present. This provides a caller with more information without any complexity or performance penalties. I suppose that thinking long and hard about one’s code may uncover such insights in a manner that TDD cannot.

  25. Good article, guess I’m getting addicted to your blog :)

    Invariants are often used without even realizing we’re actually using them. At least for me, guess now it’s almost automatic.

    A good metric of that may be the number of “assert” in ones code… doh, do this new gen wonderful languages still have an assert like thing?

    Regarding the test stuffs… test is good, but I think that testing unit shall not be written by the programmer himself, but from other people not knowin’ a thing about the code.

    Btw in the end we resolve always to “thinkin’ before acting” & KISS methodology (Keep It Short & Simple) .

    Lookin’ forward for next articles!

  26. In my University, invariants were a mandatory part of a Bachelor degree in Software Engineering (Germany).

    Forgetting about them is easy though: if all you do is programming web applications, you hardly ever hit a real algorithm, thus you never really think about invariants. There is a lot of software engineering going on that is indeed just glueing parts together.

    About the Invariants+OO part: yes, yes, and yes. And in particular yes to making everything immutable whenever possible. Unexpected state changes in objects are one of the biggest sources of programming errors.

    I was quite disappointed to see that Scala does not have any explicit support for marking an object as immutable. The D programming language is much nicer in that regard. C++ has const methods, which are kind of nice, but then it has (I don’t quite remember the keyword) volatile fields again – so nothing you can really reason about.

  27. superCat asked: “What’s a good book, language, environment, etc to be able to learn this properly“?

    That’s an interesting question in its own right. The classic answer would be something like David Gries’s The Science of Programming, 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 he avoids the techniques completely, which I think is a real loss. So probably an academic book is 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 Pearlsmay 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.

    But I’d like to hear recommendations from others who are more widely read than I am: are there other books that do a good job of expounding formal thinking-about-code tools like invariants from a practical perspective? Or does that book still wait to be written?

  28. Darius and dave, thanks for your corrections on the use on invariants in the comments to the original post. I’ve modified this one so that it now mentions the invariant comments in Darius’s code and notes that dave uses assertions. My bad.

  29. Thanks heaps for the articles to date. I’ve been posting my own solutions and gripes to the original post before just now reading the rest of the sequence. Glad that you’ve ended up talking about invariants – that’s a particular idea that I have recently become aware that I don’t use very often, so this has been a timely reminder and reinforcement for me.
    Many thanks.

  30. I think i found a bug in your example code…

    that is, the size of the array should be of type size_t or at least unsigned long (which is the same on most systems)… if someone had a really big array, your precondition fails due to a variable overflow

  31. Colin Wright

    Your code passes all but one of my (overly rigorous) test suite, which is well done. It shows the strength of using invariants, while at the same time showing that unless you have invariants or tests for *everything* that might go wrong, things can still go wrong.

    Let me know if you want to know the bug I found.

  32. Luxifer,

    I could have used size_t for the array size, yes; but I didn’t want to unnecessarily confuse non-C/C++ programmers with that bit of language-specific arcana. The point here is the derivation and correctness of algorithm.

    (Maybe I should have used pseudo-code to avoid this sort of thing.)

  33. Colin, yes, of course I want to know what the alleged bug is!

    (But my guess is that it will turn out to be something out of scope, like coping gracefully with a null array-pointer.)

  34. Mike,

    On saturday I started teaching myself C++ and yesterdays topic for me was complex variable types and when your “Yes, I realise that I am setting myself up for a really big fall if someone finds a bug in it!” motivated me that was the first thing I’ve noticed ;-) Sorry for pointing on such a thing when I know that wasn’t the point…

    BUT that may be a point in a future article, don’t you think? I mean, setting unsuited variable types can lead to bugs which are hard to find.

    Regards,
    luxifer

  35. Colin Wright

    Bug. OK.

    If the size of your array is MAX_INT and the items in the array are all less than the item you seek, you eventually add 1 to MAX_INT, underflow, and access an element that doesn’t exist.

    There is a simpler invariant and simpler code that together have a few advantages:

    1. No overflow or underflow problems

    2. Finds the first element among those that compare equal

    3. Has only two cases to branch between and not three.

    On the downside it still does log(n) comparisons even if it finds the desired key on the first comparison.

  36. Colin suggests:

    If the size of your array is MAX_INT and the items in the array are all less than the item you seek, you eventually add 1 to MAX_INT, underflow, and access an element that doesn’t exist.

    Nice try, but no. If the size of the array (i.e. number of contained elements, including a[0]) is MAX_INT, then the variable upper is initialised to MAX_INT-1, not MAX_INT. Then as the search progresses, lower is increased until the range is emptied, i.e. it takes the value upper+1, which is when the loop exits (and -1 is, correctly returned). Because upper was set to, and still is, MAX_INT-1, lower is set to (MAX_INT-1)+1 = MAX_INT, and no overflow occurs.

    Just in case I missed something, I also tested this (using unsigned char as the index type rather than int, as I don’t want to make a two-billion-element array). Sure enough, it correctly returns -1 when searching for the value 1 in a MAX_SIGNED_CHAR-element array where all elements are zero.

    So … either there is a bug in your “(overly rigorous) test suite”, or you didn’t actually run the tests … which is it? :-)

  37. Colin Wright

    Ah, I see. Even though C allows one to have an array indexed from 0 to MAX_INT, your code doesn’t permit it. Your code requires that the last index is MAX_INT-1. That means you can’t get the overflow, at the cost of not allowing an array of the maximum size the language permits.

    That’s neat, but it’s also a “gotcha” in your code that might be worth a comment.

    My test suite uses a slightly different spec for the search function, so I had to rework your code. The reworked code isn’t limited to an array of ints, and uses a generic “cmp” function. The spec I wrote specifically says that the routine has to work with arrays indexed from 1, so I had to change that too.

    So neither of your suggested options is correct 8-) I don’t have a bug in my test suite (that I know of!), and I did actually run it. I have the code I ran, based on your code, and the full test results in case you’re interested.

  38. Colin says:

    Even though C allows one to have an array indexed from 0 to MAX_INT, your code doesn’t permit it. Your code requires that the last index is MAX_INT-1. That means you can’t get the overflow, at the cost of not allowing an array of the maximum size the language permits.

    That’s not really right either. Remember that it’s perfectly valid for a C implementation to have 16-bit int and 32-bit size_t, so it’s absolutely the case that you can make arrays in C that an int can’t fully index. For that matter, even a 32-bit (signed) int can’t index more than half of what a size_t can.

    Simply, the code given in the article works correctly for a sorted array of any size up to the largest that the size parameter can represent. If you want a bigger array than that, just rewrite using a more capacious type for size, lower, upper and i (i.e. all the variables that count the size of, or index into, a[]).

    But, as interesting as all this is, it has no direct relevance to the actual algorithm, which is what I’d prefer to focus on — I think we could all improve our code much more by better understanding of algorithms than by detailed consideration of MAX_INT edge-cases :-)

  39. Colin,

    > Ah, I see. Even though C allows one to have an array indexed from 0 to MAX_INT, your code doesn’t permit it. Your code requires that the last index is MAX_INT-1. That means you can’t get the overflow, at the cost of not allowing an array of the maximum size the language permits.

    You’re wrong. Array indexing starts at 0, so even if sizeof(array)==MAX_INT the last index of the array is MAX_INT-1…

    Maybe you should reconsider your reasoning in this case :-)

    example:
    if MAX_INT was 3 that would mean an array could only have 3 elements a[0], a[1] and a[2]

    in mikes function, upper would be 2 and lower would max out at 3, which is perfectly valid…

    please tell me, if i’m missing something here…

    cheers

  40. Oh, and Colin also said:

    My test suite uses a slightly different spec for the search function, so I had to rework your code. The reworked code isn’t limited to an array of ints, and uses a generic “cmp” function. The spec I wrote specifically says that the routine has to work with arrays indexed from 1, so I had to change that too.

    So what you’re saying is that you took the code that I claim to be correct, modified it, ran the modified version, and found that the modified version overflows?

    So neither of your suggested options is correct 8-) I don’t have a bug in my test suite (that I know of!), and I did actually run it.

    Yes — for some value of “it” that is not the code that I actually wrote!

  41. Binary search is one of a class of problems in which the expression of the problem is very simple, but the implementation is very sensitive to getting the boundary conditions right.

    An inductive proof using loop invariants can make it very clear what the boundary conditions should be. Testing only reveals that you have them wrong.

    A reliance on testing, rather than on analysis, can result in a solution that is far more complicated. That relies on coding for special cases, rather than on creating code in which the general case handles all of the special cases correctly.

    Bentley has another great article in that book on loop invariants, and that should be a “must read” for all developers. Every loop that you ever write should be analyzed, at least informally, using induction and loop invariants. (Unless, of course, it is of exactly the same form as a loop for which you’ve done such analysis in the past – which most of the loops you write will be,)

  42. Arild Haugstad

    Commenting on the ongoing discussion, it appears that we have the following fundamental conflict:
    “Obviously”, with the array indexed by an int, an array where the last index is MAX_INT should be legal.
    Simultaneously, “obviously”, with the array size specified by an int, an array with more than MAX_INT element should not be legal.

    Personally, I find the later point “more obvious” than the former — though even if it wasn’t so, I would argue that the code isn’t directly buggy: It demands that the “size” parameter specify the array size. For an array of size MAX_INT+1, it is thus not possible to call the function. This input constraint is clear from the type signature of the function, and should not come as any surprise. It may be argued that this constraint is unfortunate, but unless we start indexing from 1, the problem won’t go away as long as the same numeric type is used for size and index…
    (In practice, we might use a size_t, and we should be “safe” — as the program would then run out of addressable memory before hitting the edge case…)

  43. Excellent post – thank you.

    I don’t have a CS degree, but it turns out invariants are a formalization of what I’ve always thought of generically about “thinking clearly about what an algorithm does.” Having the concept formalized is a great help.

    I really learned to do this when I first learned Clojure. Recursion and iteration are formally equivalent, but I think recursion *forces* you to think in terms of invariants – with an algorithm implemented recursively, the actual invariants are encoded into the recursive function’s signature.

  44. Phillip Howell

    The ability to reason rigorously about a program depends on having solid knowledge of its relevant state, and what is an “object” but a big opaque ball of mutable state that can change under our feet?

    So, here are these things called “class invariants.” They’re sort of like invariants, but, you know, for classes. Just like algorithmic invariants: if a class invariant becomes untrue, the code is broken. All methods of the class must preserve the invariant.

    So, no — if you’ve done your thinking correctly and have the right invariants, an object is *not* a big ball of immutable state.

    Most people miss that first step, regardless of what kind of code they’re writing.

    [I kind of hate having to be an OO apologist here: I've seen about the same ratio of good:bad OO code as good:bad procedural code in my professional life. But you keep talking about bad OO code as if it were all OO code.]

  45. Luke V,

    I was also thinking about the relationship between loop invariants and recursion. I don’t think it’s correct to say that the invariants get encoded into the recursive function’s signature, but I’m not how to put it better.

    Maybe it’s better to say that there aren’t really invariants, there are just pre-conditions and post-conditions for the function. Recursion forces you to (1) identify the base cases (2) ensure that the post-condition is satisfied for the base cases (3) reduce the problem to a smaller size that still satisfies the preconditions. Then proof by induction tells you that the post-conditions will always be true.

    You end up going through much the same logical thinking as with the loop invariants, just coming at it from a different direction.

  46. Phillip Howell: yes, class invariants would a big help. If anyone used them, that it. I don’t know about you, but I very rarely if ever see them used. For example, having read Refactoring very recently, I can tell you that they do not crop up anywhere in that text — which seems pretty astounding on the face of it, given that you’d think well-defined class invariants would be one of the most useful tools for giving you confidence that your refactorings are correct.

    So maybe my new mission in life is to make people aware of class invariants.

  47. weichi, I think your analysis is about right. Invariants in the sense that I described them here are useful primarily for understanding the behaviour of loops, specifically the state at the top and bottom of the loop. But when a function is recursive rather than iterative, each time through the loop is a new invocation, so the function’s precondition and postcondition are, in essence, the invariant at the start and end of a go around the loop.

    Another way to think of this is that a loop invariant is merely a special case of a precondition for a code fragment (the loop body) and the postcondition of the same code fragment, that happen to be the same.

    Of course, I haven’t talked about pre- and post-conditions yet (they will be part 3, after bound functions), so we are cheating a bit by jumping ahead :-)

  48. Colin: “The spec I wrote specifically says that the routine has to work with arrays indexed from 1, so I had to change that too.”

    If you’re writing in C and defining a spec with one-based indices, you’re introducing bugs. Fix your spec.
    Zero-based arrays not only match the idioms every C programmer in the world expects to see, but they also make boundary errors of the type you introduced a lot less likely by matching the range of fixed-width integer types more naturally.

  49. Colin Wright

    dave : “If you’re writing in C and defining a spec with one-based indices, you’re introducing bugs. Fix your spec.”

    With respect, some programmers don’t have the luxury of designing the interfaces they use, but simply have to get on with writing code to use the interfaces they’re given. The challenge I had set was intended in part to see if people could, or would, read the spec, or whether they would simply plough on and write code using their own expectations.

    Many bugs in the real world arise from people not properly reading the spec and writing code to do what they think the spec should say. Those are still bugs.

    There’s more to writing correct code than knowing and using the idioms of the language, and while it’s important in general to try to go with the code rather than against it, there are times when there are impedance mis-matches and you have to do what you can.

  50. Phillip Howell

    Thinking more on this post, I’m going to make an assertion triggered by the following comment:

    I’m going to claim that this code is objectively better than most of the solutions that were posted in response to the original challenge

    I assert that your solution is inferior to every correct recursive solution presented., because binary search is a naturally recursive algorithm, and we should express the implementation of algorithms in their most natural forms.

    I’m not entirely certain that this assertion is correct, even if the reasoning behind it is correct; and I’m not certain of that, either.

    That being said, it’s not clear to me why anyone would ever implement a naturally recursive algorithm iteratively except to confuse future readers. (And don’t say performance; any self-respecting compiler is going to convert tail recursion to iteration.)

  51. Finishing my 3rd year up over here on the West Coast of the States, and I don’t recall anything about invariants in my coursework. Granted, I intentionally forget most of what I learn in uni to make way for things more useful to me, but it doesn’t ring a bell.

  52. Colin: “With respect, some programmers don’t have the luxury of designing the interfaces they use, but simply have to get on with writing code to use the interfaces they’re given. The challenge I had set was intended in part to see if people could, or would, read the spec, or whether they would simply plough on and write code using their own expectations.”

    And who, exactly, gave Mike the spec he was writing to? (Hint: It wasn’t you.)

    Programmers do at least have the luxury of seeking other employment when they find themselves working for idiots, and that’s exactly what I’d do if the people who pay me for my time treated me the way you’re treating Mike.

    (But since I’ve given up arguing with people on the internet, this is the last you’ll be hearing from me.)

  53. Another note from a recent graduate (2008). I asked a fellow CS graduate from Rutgers in NJ if I’d forgotten those topics or if they were never covered, he said he’d never heard of them before. I remember a TA lament once that his students (my peers) had never studied pre- and post-conditions or formal proofs of correctness. I had never heard of invariants until I started reading “Coders At Work.” Sounds like I might be in the minority from skimming the comments. Anyway, thanks for this post, it’s a nice introduction beyond the Wikipedia page (although that page actually has a pretty clear example too). Between this and the binsearch series I’m now officially a “regular reader.” Have to cast a vote against those slabs of cow though (vegan), the sushi was at least pretty and smaller.

  54. Colin Wright

    I said: “… some programmers don’t have the luxury of designing the interfaces they use …”

    Dave: “And who, exactly, gave Mike the spec he was writing to? (Hint: It wasn’t you.)”

    No, that’s true, he was writing to his own spec. I’m not sure why you think that’s relevant. What I did was take his code, make minimal changes to it to match what appears to be an equivalent spec, including making the adjustment for the indexing from 1, and then ran it through a test suite I happen to have handy.

    It found a problem.

    As it happens, the problem wasn’t in the change for the re-indexing, and it wasn’t in Mike’s code. I have said as much already.

    Dave: “Programmers do at least have the luxury of seeking other employment when they find themselves working for idiots, and that’s exactly what I’d do if the people who pay me for my time treated me the way you’re treating Mike.”

    If Mike feels I’ve treated him badly then I apologise unreservedly. Such was very far from my intent. I was hoping to add constructively to the discussion, to point out a place where code very similar to his fails, and to discuss the points that arise from that.

    If Mike feels that I’ve done that badly, or that I’ve been obnoxious, unfriendly, or otherwise anti-social, then he can have a full and complete retraction.

    Dave: “But since I’ve given up arguing with people on the internet, this is the last you’ll be hearing from me.”

    Arguing and discussing are different things. I feel that you’ve mis-understood me, and that’s a shame. It feels like you’ve taken offence on Mike’s behalf, shouted and me, and are now going off in a huff (possibly in a taxi and a huff, or possibly in a coat, a taxi and a huff, but that’s another story).

    I’m sorry you feel you can’t discuss things, I’m sorry you feel that it’s an argument. I do feel you’ve not understood what I’ve been saying, and regret that I wasn’t able to make myself clearer.

  55. dave said: “Programmers do at least have the luxury of seeking other employment when they find themselves working for idiots, and that’s exactly what I’d do if the people who pay me for my time treated me the way you’re treating Mike.”
    and
    Colin said: “If Mike feels I’ve treated him badly then I apologise unreservedly.”

    Thanks to you both; I appreciate dave’s defence, and also Colin’s apology; although none was necessary — this is all just the cut and thrust.

    “If Mike feels that I’ve done that badly, or that I’ve been obnoxious, unfriendly, or otherwise anti-social …”
    No, absolutely not.

    Happily, almost every single one of the 2217 comments on this blog so far has been civilised. (And neatly all the exceptions were spam, which I junked.)

  56. On the subject of the inserted photos:

    Having completely unrelated photos of colorful food between occasional paragraphs works nicely as a signature design element for your posts. If I followed a blind link (not that I’d actually do such a thing these days) and ended up viewing the middle of one of your articles, I visually know, almost instantly, that it’s probably you before reading a single word.

    The steak today is stylistically consistent with the earlier sushi pics (colorful closeups, often sliced and fanned out), and thus works fine. Carry on!

  57. Arild Haugstad

    Mike:
    To correct your as well as my own comments that you could have used a size_t for the array size:
    That could break on searching for something smaller than the first element in the array, when the “upper” is supposed to be set to a value *below* the “lower” of 0 to represent the empty range… (At which point Colins variant with indexing from 1 becomes preferable — because then, there’s no problem for arrays with “normal” sizes… (And our hardware/OS/programming language/environment is extremely unlikely to be able to allocate arrays of the “problematic” sizes, given that a size_t must be able to represent an address, and the addressable unit usually being 8-bit bytes and the array elements being “ints” that can be expected to be 16 or 32 bits… I’m overthinking this.))

    I think I’ve just been reminded why half-open ranges are usually a more elegant solution…

  58. I graduated in 2005 in France.

    The first three things I learned in my algorithmic courses in Colleges were
    – invariants, preconditions, postconditions
    – induction proof
    – complexity. Worst case/average, in time/size.

    Then we studied other things, like classical data structures (list, stacks, trees…) I remember your code or pseudo code would not be even looked at if it did not have a precondition/postcondition for each function/method and an invariant for each loop. This rule was relaxed in the 2nd year of college, but I think no one can possibly say they did not hear about invariants!

    PS: about being misinterpreted. I find your opinions very clearly expressed. Surely people are not reading your posts thoroughly, or are just trolling around. I hope that will not discourage you from blogging in the future.

  59. Pingback: Top Posts — WordPress.com

  60. You may have something in suspecting that object-orientation has distracted attention from reasoning about program correctness, as, in its popular (mis)interpretation, the focus is on state rather than algorithms (there’s a connection here to the difficulty you had, with Martin Fowler’s refactoring book, trying to figure out what’s happening, and where, in the refactored code.)

    Nevertheless, I think there are better candidate causes: the software engineering and the agile methods movements. This may appear to be a self-contradictory claim, as these are commonly considered to be antithetical camps, but they both, in their own ways, avoid the issue.

    In the popular (mis)interpretation of agility, it’s all about testing and -f-i-x-i-n-g- refactoring, and you have already refuted someone who apparently thinks so. The apotheosis of this fallacy is contained in the phrase ‘test-driven design’, which begs the question of how you can ever get a line of code to test in the first place. The answer, of course, is that you write code with an expectation that it will satisfy certain requirements (which may have come directly from the intended use of the code, or transitively via a higher-level design) and that expectation had better be well-reasoned, because you don’t have time to exhaustively test vague and uncertain implementations.

    On the other hand, in the popular (mis)interpretation of software engineering, it is all about process, and most specifically, the process for requirements specification and ‘verification’ (which, in practice, means (once again) testing). Software engineering, at least in the mainstream view of it in the US and Australia, seems disdainful of that part of software development which actually creates software; it’s a job for technicians, whose work should be measured by a set of metrics that have only a cursory, coincidental relationship to correctness. The apotheosis of this view is the CMM(I), which purports to measure an organization’s competence in software development, not through its ability to deliver working software, but by its adoption of, and adherence to, a bureaucratic set of procedures.

    Software engineers seem to have something of an inferiority complex with regard to ‘real’ (physical) engineering, which appears to be justified. It is unthinkable that someone could be an electrical engineer without understanding and being able to work with the concept of impedance (even if her current job doesn’t need that skill), and in my mind, it is equally unreasonable that someone who cannot work with invariants and pre- and post-conditions should describe himself as a software engineer.

    I have suspected that there is something of a geographical divide here, and the responses so far seem to support that: In general, European teaching seems to be better grounded in these issues than in the USA (Europe is also the home of Eiffel, where you will find support for class and loop invariants, together with pre- and post-conditions, and Erlang, perhaps the most widely used functional language outside of academe.)

    The real answer to your question, however, is that learning and working with invariants etc. is difficult. It is understandable (if short-sighted) that students and autodidacts might shy away from them, but it is inexcusable for education to do so. They are difficult precisely because they get to the heart of what is difficult about developing good software, and that is precisely why they should be taught. Education should be shaping the future, not going with the flow.

  61. Effective Java as well as Java Concurrency in practice contains discussions about invariants. It’s worth noting that the concept of invariants becomes even more important in a multi-threaded environment.

  62. Phillip Howell

    @ARaybould

    Software engineers seem to have something of an inferiority complex with regard to ‘real’ (physical) engineering, which appears to be justified.

    Most “software engineers” I’ve known — at least the good ones — don’t have an inferiority complex here because they don’t seem to think of themselves as engineers.

    Software development is not a purely engineering discipline, nor a purely scientific one, nor a purely creative one, but it combines aspects of all three of those disciplines — as well as, quite often, specific domain knowledge.

  63. Pingback: Writing correct code, part 2: bound functions (binary search part 4b) « The Reinvigorated Programmer

  64. i am a vegetarian. your pictures do not bother me at all. its likely because i am hear for the code not the food. i get really sick of the whiny, preachy vegetarians. they make me look bad and their behavior makes me embarrassed to even discuss my diet with people.

  65. @Phillip Howell: Point taken – there’s no need for me to be making disparaging remarks about software engineers, and I was only thinking of those who conflate ‘software engineering’ exclusively with ‘development process’. I do wonder, though, why your colleagues would call themselves software engineers if they don’t think of themselves as engineers — is it simply because that’s what the job is called? I had forgotten that there are two different uses of the phrase: there are those people who want to model software development on engineering, and then there is the use of the phrase to mean anyone who is developing software for embedded and other engineering purposes. My point is that I would think that people in the former group would be eager adopters of the techniques Mike is writing about, but with some notable exceptions, that doesn’t seem to be the case (I’m basing my observations on what I see written and taught under the rubric ‘software engineering’.)

  66. Phillip Howell

    @ARaybould

    I was using your term, hence the quotes. My personal tendency is to call such people [software] developers. In general, I’ve just heard “I’m not an engineer” enough from such people that I’m almost tired of it.

    From what I’ve seen of software engineering curricula (my n is admittedly 1ish here, in the US), it’s much less about actual programming and much more about the process surrounding the programming, as you mentioned in your first comment.

    And this sort of thinking makes perfect sense in fields where software must actually be engineered — nuclear facilities, manufacturing control systems, etc. Engineering is mostly about validation and guarantee.

    But real engineering is expensive, and so software developers are rarely given the time or resources to do it.

    There’s an interesting conversation of the topic over on the wiki: http://www.c2.com/cgi/wiki?SoftwareEngineering

  67. I like invariants, but still have to learn to find the invariant for a given algorithm. Mine stay invariant only at the beginning and the end (of a loop or the whole function) but do not stay invariant throughout execution like yours did.

    I checkout two books referenced in the comments (Jon Bentley and Jeff Edmonds).

    While I like to proof-read the code to find bugs, testing is still mandatory. Which tools/constructs do you recommend for the purpose for native C++ (as opposed to leaving the invariant stated in a comment)?

  68. And I still do not like pictures of food embedded in your blogs. What’s the motivation for these anyways?! :-)

    OK… Well… so when are you updating your website to allow readers to insert pictures in their comments?!

    And please, do not just replace them by pictures of non-edible items now just like you did for complaints against sushi pictures.

  69. Alok made an interesting point about invariants: “Mine stay invariant only at the beginning and the end (of a loop or the whole function) but do not stay invariant throughout execution like yours did.”

    You get to define when an invariant holds. You may need to temporarily violate it in order to perform part of your algorithm; that’s fine so long as you can still reason about it. The important point about the invariant in the binary search example was that whenever it’s true at the top of the loop, it will also be true at the bottom: it’s from that that you can deduce that it remains true throughout the lifetime of the loop, and so that you’ve not missed a hit. But if my code (for some reason) did tmp=upper; upper=9999; upper = tmp;, then the invariant would still hold for the loop, which is what matters.

    (I’ll have more to say on this when we get to preconditions and postconditions.)

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

  71. I did graduate recently (2 years ago), and not only did they not teach us things like invariants, but they also didn’t actually teach us to program. They taught us to “develop” software, by which I mean modelling and the SDLC and requirements gathering and the like. Very little time was spent on actually teaching programming. Why this is, I don’t know.

  72. George Baker

    I recently graduated from the University of Florida. There I had a wide range of curriculum in the Comp Sci program. I cant ever think of a time where any of my professors stressed the importance of the invariants, or there proper usages.

  73. Pingback: Buffy: Season 1, revisited « The Reinvigorated Programmer

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

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

  76. Prior to this, I’d never actually heard the term “invariant” before. CS major, nearly graduated, with what’s effectively a math minor (a few classes of number theory & related).

    Having said that, the concept was covered in my Theory of Algorithms class, and a short exercise was doing this exact same problem. I think most of the class got it, first try… but that’s a 450 level class, and *everybody* had encountered a binary search a few times before in earlier classes, even if they had not actually programmed one.

    We had a *fantastic* teacher, easily my favorite through all my education. Ridiculously challenging, and taught the fun stuff like algorithms and neural networks :3

  77. I just stumbled on this article, about how the Brooklyn College of the City University of New York has recently added program correctness proofs as a topic in its required courses on mathematical and computer literacy for the general student, many of whom will take no further math or comp. sci. courses.

    http://www.sci.brooklyn.cuny.edu/~arnow/ED/correctnessproofs.html

    For me, the most interesting single point was that the author considers their students’ general lack of previous programming experience to be a great advantage, as they have not been ‘polluted’ with an operational view of the subject, and thet do not believe that they already know how to program.

    If they can do it at CUNY (not the most prestigious educational institution in the city (though not the least, either)) with non-technical students, I see no reason for it to be left out of any CS or IT-oriented college-level program.

  78. ARaybould, that is encouraging indeed. Let’s hope it’s not quite such a voice in the wilderness as it may appear.

  79. Pingback: How correct is correct enough? « The Reinvigorated Programmer

  80. Mike, I’m glad to see there are other people out there who care about invariants! I’ve also written some blog posts on verifying binary search functions through the use of invariants, which can be found at http://critical.eschertech.com/2010/05/05/verifying-a-binary-search/ and http://critical.eschertech.com/2010/05/06/verifying-a-binary-search-part-2/.

  81. Pingback: Pointless code « vsl

  82. Richard Brooke

    Colin states:

    There is a simpler invariant and simpler code that together have a few advantages:

    1. No overflow or underflow problems

    2. Finds the first element among those that compare equal

    3. Has only two cases to branch between and not three.

    Can you post the code so that we can see whether it’s simpler to understand and doesn’t have other flaws you hadn’t tested for that might show up if, say, the code were ported to a different language or architecture?

  83. Colin, if you’re still here: I, too, would like to see your simpler invariant, and the code that it yields.

  84. I exist – I’ll reply shortly. I’ve learned that quick replies intended to illuminate simply get picked apart for irrelevant details.

  85. I have the similiar problem about invariants like Alok.
    I still have to learn how to find an invariant for a given algorithm, but I have no clue where to start. Where to look at the algorithm?

    Is there something like a step by step way I can use to find invariants for any algorithm or literature about how to do it?

  86. Josh, I don’t know of a Magic Method for determining the correct invariant for a given algorithm. I think a more fruitful approach would be that when you’re designing the algorithm in the first place, you also design the invariant. In order to come up with an algorithm you sort of have to have an invariant in mind, however implicitly. For example, the way bubble-sort works is that one more element is put into its right order within the lower segment of the array, so that this segment grows on each time around the outer loop, so the invariant is that the slice of the array from 0 to i is sorted (and all elements are permuted from the original values). The trick is probably to make this implicit notion of the invariant explicit.

  87. @Josh, Alok et al: to understand the use of invariants, I think it helps to consider the problem that they solve.

    Given a procedure with no branches, you seek to show that the postcondition for each statement follows from its preconditions and the action of the statement, and that the preconditions of each statement are satisfied by the previous statement’s postcondition, leading to a proof that the postcondition of the procedure as a whole follows from its precondition and the aggregate action of its statements. Conditional statements are a bit more complicated, but they can be handled by cases (the postcondition follows both when the condition is true and when it is false).

    If the procedure contains a loop then, for a particular invocation, the loop is executed a specific number of times, so you could unroll it into the equivalent loop-free sequence of statements and apply the above reasoning. This is not, however, useful – what we want is a general solution that will work regardless of the number of iterations it will take, and that is where the invariant comes in (you also need to prove the algorithm will not enter an infinite loop, but that is a separate issue.)

    In a loop like

    while Cond then do Body

    where Cond is a side-effect-free predicate, an invariant is a condition that is true each time the loop body is entered. For it to be true on the first iteration, it must follow from the conjunction of the loop’s precondition and Cond, and to be true on subsequent iterations, it must follow from the conjunction of the body’s postcondition and Cond. To be useful, the invariant, together with the fact that Cond is false when the loop exits, should imply the postcondition of the loop as a whole. The invariant generally formalizes the intended purpose of the loop, so that at any given iteration, it shows what progress the algorithm has made towards satisfying the postcondition.

    Therefore you generally start designing a loop by determining the desired postcondition, and with an informal idea of how to achieve it. To take an almost trivial example, you want to find the minimum value in an array, and you plan to achieve that with something like this pseudo-code:

    for each Value in Array do if Value < Min then Min = Value;

    Your loop postcondition must require, in some way, that Min is in Array, and that no member of Array is less than Min. A suitable invariant will likely require that these conditions are satisfied for that part of the array that has been examined so far. These considerations should, we hope, alert the designer to two issues that are more often overlooked that you might expect: the initialization of Min, and whether the array could be empty; furthermore, this latter point alerts us to the fact that a useful invariant should be satisfied after zero iterations, unless that case is ruled out by the preconditions (so this is not quite a trivial example.)

    What we are doing is unrolling the loop in a generic way, just as the loop is a generic way of doing a repeated procedure. You may have noticed the similarities between this and mathematical induction. In an inductive proof, you show that if Cond is true for N, then it is true for N+1; therefore, by showing it is true for some small N (typically 0 or 1), then it is true for all larger N. This resemblance is not just a coincidence.

    You have asked for literature on the subject. Aside from searching the internet, I found ‘Error-Free Software: the Know-how and Know-why of Program Correctness’ by Robert Baber (Wiley; ISBN 0 471 93016 4) to be a straightforward and practical coverage of the basics.

  88. OK, I’ve written some thoughts here:

    http://www.solipsys.co.uk/new/BinarySearchSummary.html?reprog

    That includes the invariant I use, some code that I first derived from it, a re-write to make it easier to compare, and a final version that I think is the cleanest and clearest.

    Hope it’s of interest.

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

  90. “(Although I love Ruby, I hate the fact that it has no way to talk about these things.)”

    Ruby actually does have a way to mark variables as “const”, though I’ve never used it myself. It’s the method “freeze”. From what I remember reading, when you call some_object.freeze, any further messages sent to some_object will throw an exception of some sort.

  91. You’re right, of course, Rory. But the clumsiness of the syntax:

    foo = 10
    foo.freeze
    

    rather than

    const foo = 10

    just shows how much of an afterthought it is — how much it’s not in the core of Ruby thinking.

  92. It’s not quite the same, unfortunately. .freeze will only prevent modification of an object, not outright replacement. Try this:

    foo = 1
    foo.freeze
    foo = 2 # no warning
    foo #=> 2 # overridden

    You can kinda semi achieve const with all-caps constants:

    FOO = 1
    FOO = 2 # outputs, to stderr I believe: warning: already initialized constant TEST

    But that’s a far cry from actual const variables.

  93. People who don’t appreciate the difference between statically-checked and dynamically-checked constraints are missing something pretty fundamental about computing. Only a small, though important, subset of constraints can be statically checked, but for those that can be, static checking is infinitely better. Ruby’s freeze (as described in these comments), therefore, is not equivalent to a statically-checkable const. That does not mean it is useless, though from what Groxx says, it looks like something of a kludge (ICYHG, IANARP.)

  94. (ICYHG? Not familiar with that one)

    Not really a kludge, just a different scenario. Making an object immutable is entirely different than making a particular reference immutable, especially in a language which does not allow you to work with pointers directly.

    It’s a little strange that there are literally no constants, but that fits with Ruby pretty well – there are no closed classes, you can override any function, etc. And I’ve used the re-assign ALL_CAPS_PSEUDO_CONSTS to good effect – I wrote a better URL regex for a Rails project than it ships with, and it was a simple matter of overriding the existing value, which wouldn’t even be possible if it had real constants.

    All in all, I actually prefer no-consts for reasons like the above. If I don’t like it, I can fix it, rather than being at the whim of the library writer, who may or may not have anticipated my use-case. If you want to go deep down *that* rabbit hole, I will heartily recommend .NET to you – it’s an absolute mess of bad built-in APIs (mostly in the older versions, admittedly) that are literally un-fixable, OSS projects with bugs that you can’t fix without changing your entire compile chain to handle a different code signature, and probably a top-down / waterfall strategy’s wet dream because you can dictate what your programmers can and cannot do in great detail.

  95. I should clarify that last bit: no-consts for dynamic languages which favor flexibility and metaprogramming. For other languages / scenarios, absolutely, compile-time verification kicks ass. As do static analysis tools, which are a heck of a lot easier in more restricted languages.

  96. First, I just graduated with a degree in CS from a top 25 university, and no, they did not mention invariants that I can remember. I had to take classes on theory of computation, and operating systems, 4 calculus classes, diff/eq, 2 statistics classes, and a damn chemistry lab, but they failed to even mention what an invariant is.

    Thank you for this post, and the previous posts in the series. You explain everything so lucidly and in a logical balanced way. I will definitely be coming back often to read your stuff.

  97. Thanks, Mike, your comments mean a lot to me!

  98. Pingback: Kompetisi Master Chef « begin from badcoding

  99. Yeah.. in my Soft. Eng program they teach it (that is why I ended up here). But yeah most CS students seem to think if you just test the crap out of your code and it validates it. Our lecturer stresses that you are only testing a subset of the possible errors with that line of thinking.

  100. True, and that is not even the best argument, which I think is that it makes you really think about, and understand, what you are doing.

  101. The latest Ada standard, Ada 2012, added preconditions, postconditions, and type invariants, all checked like assertions. A massive boost in the support for invariants in the language.

  102. Excellent news, but maybe about forty years too late! All this stuff dates back to the Hoare logic, proposed back in 1969. It’s incredible to me that all this time later it’s still seen as a weird, esoteric side-road.

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