7 ms·

Loop Invariants

• mrestko 11y ago
  A few more examples would have been nice.
• yodsanklai 11y ago
  As a source of motivation for students, does anyone could point me to some "real (open source) code" where the programmer commented a loop with an invariant for clarity.
  • dilap 11y ago
    Here's binary search from Go's sort package: func Search(n int, f func(int) bool) int { // Define f(-1) == false and f(n) == true. // Invariant: f(i-1) == false, f(j) == true. i, j := 0, n for i < j { h := i + (j-i)/2 // avoid overflow when computing h // i ≤ h < j if !f(h) { i = h + 1 // preserves f(i-1) == false } else { j = h // preserves f(j) == true } } // i == j, f(i-1) == false, and f(j) (= f(i)) == true => answer is i. return i } There's lots more examples of you search for "invariant" thru the std library source code. A few, to give a taste: ast/print.go printer.Write // invariant: data[0:n] has been written printer/printer.go trimmer.Write: // invariants: // p.state == inSpace: // p.space is unwritten // p.state == inEscape, inText: // data[m:n] is unwritten path/filepath/path.go: path.Clean // Invariants: // reading from path; r is index of next byte to process. // writing to buf; w is index of next byte to write. // dotdot is index in buf where .. must stop, either because // it is the leading slash or it is a leading ../../.. prefix. Invariants really are a really useful way to think about code.
    • ufo 11y ago
      Binary search is one of my favorite examples for introducing people to loop invariants. There are tons of opportunities to mess up with an off-by-one error but if you state the invariant beforehand getting it right is super easy. There are also many variations of the binary search problem so you can't just memorize the implementation.
  • eliteraspberrie 11y ago
    Here's an example in a getline implementation: https://github.com/eliteraspberries/ttyprompt/blob/master/getline.c#L55 https://github.com/eliteraspberries/ttyprompt/blob/master/ge... /*@ loop invariant i; loop invariant j >= 0; loop assigns j, eol; */ for (j = 0; j < (size_t) i; j++) { if (read_buffer[j] == '\n') { eol = 1; j++; break; } } Loop invariants are part of the ACSL specification language, and they can be verified automatically with Frama-C. http://frama-c.com/acsl.html http://frama-c.com/acsl.html
  • mcguire 11y ago
    Weirdly, I hadn't tripped over 'loop invariant' in years, then I scribbled my own ode to them[1] and now this. Loop invariants get important in the section on Bentley-McIlroy three section partioning. [1] http://maniagnosis.crsr.net/2016/02/quicksort.html http://maniagnosis.crsr.net/2016/02/quicksort.html
• mhd 11y ago
  This reminds me of Eiffel, where loop (in)variants had to be explicitly declared, as part of its design-by-contract dogma.
  • phpnode 11y ago
    I wrote a Babel plugin which brings a similar syntax to JavaScript, so you can write this: for (let i = 0; i < someVar; i++) { invariant: i < 10000; console.log(i); } along with other kinds of contract, like preconditions and postconditions - https://github.com/codemix/babel-plugin-contracts https://github.com/codemix/babel-plugin-contracts
• PaulHoule 11y ago
  One of the things I find funny is that the halting problem is the least of my concerns working in mainstream programming languages today. Maybe back in the day when people were using basic and assembly language it was easy to write some gawdawful mess but since structured programming I think it is easier to do the right thing rather than the wrong thing. Partially because we have good constructs to work with, secondly they are good constructs to reason with -- for instance, you might have the idea of a loop invariant in your head when you write the loop, even if you don't call it that.
  • deleted 11y ago
    [deleted]
  • ufo 11y ago
    The halting problem is just an example. The real concern is that any "nontrivial" program property is also undecidable (see Rice's Theorem)
    • Animats 11y ago
      That's incorrect. Rice's theorem only says that it is possible to construct programs for which "nontrivial" program properties are undecidable. But you don't have to construct undecidable programs. In fact, you have to work at it to write a useful but formally undecidable program. (Also, you need infinite memory to get theoretical undecidability from a deterministic system. With finite memory you eventually have to halt or repeat a state.) The people behind the Microsoft Static Driver Verifier say that they are unable to decide if a program is safe to be a kernel driver about 4% of the time. This is grounds for rejecting the driver. If your kernel driver is anywhere near the limits of formal decidability, it shouldn't be in the kernel. Typically, you fix undecidability by adding loop counters or checking. If you have some complex algorithm where termination is hard to prove, adding a loop counter and an iteration limit will guarantee termination. (This comes up as a practical matter in floating point work. There are algorithms which are guaranteed to terminate on real numbers, but not on finite-precision floating point numbers. One example I've run into is GJK, used in collision detection.) Undecidability is just not a problem in real program verification.
• deleted 11y ago
  [deleted]
• Rhapso 11y ago
  If I made a zeno's paradox loop: bigFloat delta = 0.5 bigFloat total = 0.0 while total < 1.0: total+=delta delta*=0.5 Where does this fit in the model of using a loop invariant to show the loop terminates? The loop is always approaching the terminal case (and eventually the machine runs out of memory)
  • deleted 11y ago
    [deleted]
  • emillon 11y ago
    This kind of proofs usually are separated in two steps: - correction: define a loop invariant. Assuming the loop terminates, it will hold when the program exits the loop. - termination: define a loop variant, something that changes at every iteration. If you can find a variant that is a strictly decreasing sequence of natural numbers (or an increasing, bounded sequence), you've established that the loop terminates. Once you've done these two steps you know that the program terminates and the invariant holds at the end. (in your case, you won't be able to find a good variant - depending on the floating point semantics you use of course).
  • spacehome 11y ago
    The two loop invariants would be: 1.0 == total + delta * 2 and delta > 0, so the while condition would never be false. The amount of memory required to store the delta variable should be at least log_2(n) bits, where n is the iteration number. This has to be true, regardless of the implementation details of bigFloat because delta has to take on n distinct values. Eventually it exhausts the memory of the machine. It seems pretty straightforward, unless your compiler is smart enough to see what's going on and optimize the body of the loop away, in which case it wouldn't terminate.
  • AnimalMuppet 11y ago
    You're asking for a loop invariant to prove that a non-terminating loop terminates? That seems... somewhat contradictory. Either you can't prove that with a loop invariant, or the proof must be invalid. As you said, the machine eventually runs out of memory. But "loop invariants" don't usually include the machine running out of memory as the termination condition, because that's more a crash than a loop termination. (That is, whatever part of the program you wanted to execute after the zeno loop won't execute, because the program terminated, not just the loop.) So when we talk about loop termination, program-crashing events are usually out of scope. (That's something we also need to prove - no undesirable side effects - but that's actually a separate issue.)
• justinsaccount 11y ago
  > If the current comparision shows a smaller value, we update smallestSoFar. if ( a[smallestSoFar] > a[nextToCheck] ) { This code makes me twitch. Finding a smaller value by checking to see if the old value is larger than the new value... Instead of checking to see if the new value is smaller than the old value. Additionally, calling the value you are currently checking 'nextToCheck' is also confusing. It's not the next one, it's the current one.
  • jjaredsimpson 11y ago
    a > b is the same as b < a and I would argue a > b is clearer in this instance by noting the symmetry of the following line: if ( a[smallestSoFar] > a[nextToCheck] ) { smallestSoFar = nextToCheck ; } When a > b then a = b The order of the variables doesn't change. The value is called nextToCheck because the article is specifically talking about loop invariants. The value of nextToCheck only makes sense when loop invariant is established prior to the loop and after work has been done in the loop to reestablish the loop invariant. In both of those cases the value in nextToCheck is clearly meant to denote the half open interval [0, nextToCheck) which contains the smallestSoFar. currentComparisonIndex is not the correct name for the loop variable because that name is only accurate after checking the termination condition and prior to incrementing. This is not what the loop invariant states the purpose of nextToCheck is. Therefore you would not have established a proper loop invariant prior to entering your loop. nextToCheck might more fully be called 'nextToCheckAfterTerminationCheck' Of course this is all meta above the level of the language is self. You could call the variable 'foo' and of course the code would still function.
    • justinsaccount 11y ago
      It must be a mathematician thing. When I am doing something that involves finding a smaller number, I expect to see a < operator. How would this look if you were writing code that dealt with something like a linked list where you have 'cur' and 'next' pointers? 'cur' would be 'next' and 'next would be 'nextNext' ?
      • 11y ago
• tmerr 11y ago
  Hey, this seems like an application of induction. You choose some property you want to prove about your program, show it is true before the loop (base case), then show it remains true for any next iteration (inductive step), therefore it is true for all iterations. It reminds me of the hand-wavy inductive proofs I run through my head when I write recursive functions. Usually it's not even about eliminating bugs, it's just the most natural way to understand why the code works. It seems less natural for imperative for/while loops but still a good tool to keep in mind.
  • mcguire 11y ago
    That's a good point. But then, tail-recursive functions are loops, so I guess I should have expected the correspondence.
  • Animats 11y ago
    Of course it's proof by induction. You prove that it's true for iteration N+1 if it was true for iteration N. You prove that it was true for iteration 0. Then you're done. Here's how we did it in the Pascal-F verifier [1] around 1980. This is the simplest example - proving that all entries in an array are zero after the array is initialized. type tabix = 1..100; type tab = array [tabix] of integer; rule function allzero(a: tab; i,j: tabix): boolean; begin end; var table1: tab; i,j: tabix; ... for i := 1 to 100 do begin table1[i] := 0; assert(allzero(table1,1,i-1)); state(allzero(table1,1,i)); end; assert(allzero(a,1,100)); ... assert(table1[j] = 0); { table1[j] must be 0 } The loop invariant is state(allzero(table1,1,i)); which says that the predicate "allzero" is true for table1 from 1 to i. "allzero" is defined in the Boyer-Moore theorem prover as a recursive function. (defn allzero (a i j) (if (lessp j i) t (and (allzero a (add1 i) j) (equal (selecta! a i) 0)))) That's a recursive function. The prover is able to prove that it terminates. "(selecta! a i)" is LISP for "a[i]" here. We need three theorems about "allzero". First, that it's vacuously true for j < i: (implies (and (arrayp! a) (numberp i) (numberp j) (lessp j i)) (allzero a i j))) Notation: "arrayp!" is true if the item is an array. "numberp" is true if it's an integer. "lessp" is "<". Then that it's true for a single element if that element is zero: (implies (and (arrayp! a) (numberp i) (numberp j) (equal i j) (equal (selecta! a i) 0)) (allzero a i j)))) And finally, the hard one, that if it's true up to N, and a[N+1] is zero, it's true up to N+1. (implies (and (arrayp! a) (numberp i) (numberp j) (allzero a i j) (equal (selecta! a (add1 j)) 0)) (allzero a i (add1 j)))) These are all proved, once, with the Boyer-Moore theorem prover. Once proven, they can be used as rules by the much simpler and faster Oppen-Nelson prover built into the Pascal-F verifier. Over time, you build up a library of such rules, which are applied automatically by the fast prover. This is 1980 technology; there's been a lot of progress in the last 35 years. This ran on a 1 MIPS VAX 11/780 and later on Sun II workstations. Back then, it was very slow to do this. That's a solved problem. It's still rather painful. But it works. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf