11 ms·
Loop invariants can give you coding superpowers
- eschneider 8y agoInteresting article, but if one considers the possibility of overflow, the invariants in some of the examples aren't true. Which doesn't mean the article is _wrong_ so much as it demonstrates one needs to prove the invariants are actually true.
- lifthrasiir 8y agoSeveral static analyzers (like Frama-C [1]) can extract loop invariants and try to prove them, giving you the best of both worlds. [1] https://frama-c.com/ https://frama-c.com/
- jerf 8y agoOn a similar note, for max and min algorithms you actually do have a sensible initial element, which is the min or the max integer for the integer type in question. However, you have to make sure this value can't escape into the caller's context (unless it really is the max value); calling max or min with an empty list ought to be an error in whatever the appropriate local error idiom is. The article (reasonably appropriately) glossed over that.
- univerio 8y agoThis is a great technique; I learned it in David Gries' Intro to CS at Cornell, but a lot of my classmates didn't think so, which elevated this to meme status at Cornell: https://quotes.cs.cornell.edu/quote/1369/ https://quotes.cs.cornell.edu/quote/1369/
- deleted 8y ago[deleted]
- lkuty 8y agoLearned that and the "weakest precondition" stuff from Pierre-Arnoul de Marneffe in 1994 at the University of Liège (ULg). Very useful but we didn't grasp the full power of it at that time.
- Jtsummers 8y agoWe had a course at Georgia Tech called "Introduction to Proofs" or something for the CS students that introduced these as well. But it was so early in our education and so separated from the programming courses that it wasn't obvious to most of us how it'd be used. It wasn't until much later that I understood these ideas and could apply them. It needed to be better integrated into the other courses (to provide motivating examples of these methods and techniques).
- Reisande 8y agoThis isn't necessarily a new idea. Tony Hoare discussed the idea for a while with his creation of Hoare triples; we are learning about the application right now in my Software Foundations course. It has a lot of interesting application within Coq for the analysis of the validity of programs, though. A good place to learn more about the application is here: https://softwarefoundations.cis.upenn.edu/current/plf-current/Hoare.html https://softwarefoundations.cis.upenn.edu/current/plf-curren...
- raincom 8y agoIs there a list of loop invariants for algorithms that are frequently used in interviews?
- 0x8BADF00D 8y agoNot sure what you mean by your comment. You can use loop invariants when solving problems that call for an iterative solution.
- jonsen 8y ago“Can you write code to reverse a linked list in place?” “Sure, I’ll just implemment a loop according to this invariant ... “ Would be nice to have the invariant ready then.
- raincom 8y agoLoop variants for popular problems and popular algorithms to solve problems. This can give us inductive way of looking various problems. And classify problems/algos based on invariants.
- hackermailman 8y agoLot's of material around on invariants for anybody interested Cornell: Invariants Playlist: https://www.youtube.com/playlist?list=PLTD_NtzzD4VC6l2uLdzbsm9wW21mMaWwj http://www.cs.cornell.edu/courses/cs2110/2017sp/online/loops/01aloop1.html https://www.cs.cornell.edu/courses/cs1110/2018sp/materials/loop_invariants.pdf CMU: https://www.cs.cmu.edu/~15122/handouts/01-contracts.pdf http://www.cs.cmu.edu/%7Efp/courses/15122-s11/recitations/recitation02.html (former CMU prof) https://www.youtube.com/watch?v=lNITrPhl2_A Of course if you really wanted to understand the challenge of finding loop invariants, there's the software foundations series of books which even if I don't understand all of it, has been still worth my time to go through https://news.ycombinator.com/item?id=19565365 https://news.ycombinator.com/item?id=19565365 and Cornell has some good introductory Coq material https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tact...
- jonsen 8y agoCornell: http://www.cs.cornell.edu/courses/cs2110/2017sp/online/loops/01aloop1.html http://www.cs.cornell.edu/courses/cs2110/2017sp/online/loops... https://www.cs.cornell.edu/courses/cs1110/2018sp/materials/loop_invariants.pdf https://www.cs.cornell.edu/courses/cs1110/2018sp/materials/l... CMU: https://www.cs.cmu.edu/~15122/handouts/01-contracts.pdf https://www.cs.cmu.edu/~15122/handouts/01-contracts.pdf http://www.cs.cmu.edu/%7Efp/courses/15122-s11/recitations/recitation02.html http://www.cs.cmu.edu/%7Efp/courses/15122-s11/recitations/re... (former CMU prof) https://www.youtube.com/watch?v=lNITrPhl2_A https://www.youtube.com/watch?v=lNITrPhl2_A
- raincom 8y agohttp://cseweb.ucsd.edu/classes/sp05/cse101/JeffEdmondsBook.pdf http://cseweb.ucsd.edu/classes/sp05/cse101/JeffEdmondsBook.p... Jeff Edmonds' "How to Think About Algorithms: Loop Invariants and Recursion" is a nice book.
- maweki 8y agoI think both for sum and max a better invariant should include the uncalculated part. Sum(0..X)=Sum(0..i)+sum(i+1..X) with the moving i. So it is true at first because the unsummed part is empty and the missing part is the goal. Then we take away an i from the solution to-go pile and put it on the done pile and when the loop has done X the to-do pile is enpty and per invariant the done pile equals the goal. Including the goal in the invariant sometimes gives you nicer properties. The equivalence relation often also implies an algorithm. For max I would say the equivalence is: Max(0..X)=Max(Max(0..I),max(I+1..X)) This of course only easier if the max of empty is negative infinity. Then you can move the i from 0 to X.
- jonsen 8y agoYou are merging the invariant with the variant. The loop invariant is supposed to tell about the state of the variant at any loop start. The variant in this case is the tupple (i,sum). Your version does not say anything about the stepwise evaluation of the sum.
- maweki 8y agoOf course this tells me about the state of the variant. And it's the same invariant the author uses but with the equation balanced differently. The author's invariant is Sum = 1+2+..I Mine is Sum+(I+1)+...+X = 1+2+..I+(I+1)+...+X That's both fine and tells us about I. I think the version that contains the value we want to obtain is easier to prove correctness for.
- GuiA 8y agoThe article describes the concept of a loop invariant and gives examples for a few algorithms, but unless I am missing something, it is not giving you any way to computationally verify those invariants? (I guess I am a bit surprised by the short length of this article because when I write code, I tend to think of it in those terms already, so I expected it to go further; but I guess not everyone has been exposed to that idea or taught to program like that in the first place so I realize that that's my own bias). What should I check out if I want to be able to formally check invariants for e.g. my Python or Swift code?
- hooya 8y agocheck out: https://en.wikipedia.org/wiki/Formal_methods https://en.wikipedia.org/wiki/Formal_methods I ran into loop invariants in my CS undergrad where they were teaching "formal logic" to prove correctness of programs. At the time, it was a bit above my head and i struggled with it. i'm just beginning to understand what it was that we were studying at the time. cool stuff. wish i could go back and re-learn that stuff. Also google TLA+ - there's a book on it by Leslie Lamport.
- Itaxpica 8y agoWhen we covered this in my CS 101 class back in the day, our professor actually had a system he had put together built on Python's unit testing infrastructure. Really, any construct in a programming language that lets you say "assert that this thing is true and if it isn't, do something" can be used for loop invariant checking.
- jonsen 8y agoLoop invariant checking should assert that if the invariant is true before the loop starts, it will also be true at the end of the loop. That’s not a general capability of assert constructs.
- skrebbel 8y agoI think there's an opportunity to name variables after their invariant. For example, in the typical sum example, the mutated variable is usually called "sum" or "total". But you could also call it sum_from_0_to_i, and then a reader can immediately see that the result is the full sum because i equals the array length. It's like a proof-by-variable-name. The same trick tends to work as well with less trivial invariants. You get long variable names, but not horribly so. You can do the same for the accumulator in a reduce/fold operation. Way too often variables in reduce calls (and other recursive functions) have horrible names, making the entire reduce needlessly hard to understand. Naming the accumulator properly solves this: Eg const total = array.reduce( (totalUptoPrevious, current) => totalUptoPrevious + current, 0 ); So much easier to follow! I've often had to look up, when reading a reduce, which argument is the accumulator in this particular language or library. When you use the invariant for the accumulator name, you fix this entirely.
- ummonk 8y agoI mean generally I tend to prefer operations that are commutative and associative, so it really doesn't matter which one is the accumulator. But I still really like your naming, it seems to bridge the gap in making reduces (which are conceptually cleaner) understandable to people who are used to iterative code.
- whatshisface 8y agoFloating point sums are one example of a place where the only usable operator doesn't commute.
- wsxcde 8y agoIf you're interested in playing around with loop invariants for non-trivial programs, I recommend the Dafny programming language which can automatically verify the invariants using SMT solvers. (Dafny is much more convenient that messing around with operational semantics in Coq.) There's a tutorial + web interface at: https://rise4fun.com/Dafny/tutorial/Guide https://rise4fun.com/Dafny/tutorial/Guide. The official repository is here: https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny -- you might want to switch to a local installation once the online tutorial whets your appetite. A good initial challenge, once you've gotten past the baby stuff in the tutorial, is implementing insertion and deletion on a binary search tree with appropriate pre- and post-conditions.
- Profan 8y agoYes! Dafny puts this stuff front and center, it's all well and good to think about invariants, but if they're just expressed in a comment and not actually verified, they might as well be filler text! If there's anything I hope the mainstream adopts at some point, it is some variation of what Dafny offers here.
- robotresearcher 8y agoThe article has invariants in comments. I like to put invariants in assertions so they get checked at run time. I know this is common practice but I haven’t seen it mentioned here and it might help someone. edit: Jonsen's reply question, for which I don't have an answer, is instructive: these loop invariants are often impossible or impractical to achieve in assertions. I modified the above to be less wrong.
- jonsen 8y agoHow would write an assert for the sum loop invariant?
- deleted 8y ago[deleted]
- raphinou 8y agoI discovered the power of loop invariants during a course at university. A professor even developed a compiler like this, starting by defining invariants and writing the code accordingly. Really inspiring! I wonder, are there such techniques tailored to functional programming? (immutability, recursion,...)
- 40acres 8y agoUdi Manber's book on algorithms and induction is also a great resource to learn about invariants. Invariants and induction go hand in hand.
- asark 8y agoTo sum (haha) up, I am no n00b. However, I've looked over the page a couple times and still can't figure out the use of this, let alone what "superpowers" it may grant. It's just comments? The best parts I can see are the mostly-prose ones farther down that just say what the loop's supposed to do, but even those are just repeating the "input" and "output" info, really, which are sort of also comments I think. Some of this might be useful if you could express it in types or some other machine-checkable fashion, but in comments they're just kind of redundant and, like any comments, must be treated with suspicion anyway. What am I missing? I just have no idea what I'm looking at here, or rather I think I do but I'm entirely missing why it should be in any sense exciting which leads me to think maybe I don't.
- repler 8y agoYou're not missing anything - it's 100/200 level computer science. (Freshman/Sophomore)
- asark 8y agoYeah I'm just getting "if the loop can be expressed as induction you can... write that in a comment, for some reason". Alright, that's nice. Could we express that as tests instead plzkthx? So I thought I must be missing something.
- jacoblambda 8y agoFor the rare languages that support invariants (or has a library that implements invariants) you would write it as code rather than a comment and the compiler will compile time error if the compiled code is capable of violating the invariant.
- Jtsummers 8y agoAnother place to use this is if you're designing a new bit of code and want to write the design out before you write the code, rather than code first (or as the code is being produced, where at times it's non-executable because you have holes in the program that are filled with these textual descriptions). You could put some of these into asserts or similar. Like for the three way partition. Create an assert that at each iteration the array[:low] values are all less than p, array[high:] values are each greater than p, and array[low:mid] values are each equal to p. If it doesn't hold then you know your code is wrong. This does induce a performance hit, but asserts can be turned off for deployed code.
- 0815test 8y agoLoop invariants are a lot more intuitive if you convert your loops into while() form and then further into tail recursion - they turn into a proof by induction. For the first example, consider: go (n, i, sum): given sum = 1 + 2 + ... + i-1 returns (1 + 2 + ... + n) : per cases of (i <= n) assume (i <= n) { note: (sum = 1 + 2 + ... i-1 -> (sum + i) = 1 + 2 + ... + i) return go (n, i + 1, sum + i); } else assume (i > n) { note: thus i = n + 1 then: sum = 1 + 2 + ... + i - 1 = 1 + 2 + ... + n return sum; } sum n: returns 1 + 2 + ... + n = { note: 0 = 1 + 2 + ... + (1 - 1) // ^^^ Need to prove our precondition for go! return go (n, 1, 0); } The other examples are a bit more complex for sure, but structurally similar. It's nonetheless easy to see how even very limited changes in complexity (such as the choice of loop indexing) can create quite a few pitfalls for truly rigorous proof!
- seagullz 8y agoThe following anecdote is from https://courses.csail.mit.edu/6.042/spring18/mcs.pdf https://courses.csail.mit.edu/6.042/spring18/mcs.pdf: The Invariant Principle was formulated by Robert W. Floyd at Carnegie Tech in 1967. (Carnegie Tech was renamed Carnegie-Mellon University the following year.) Floyd was already famous for work on the formal grammars that transformed the field of programming language parsing; that was how he got to be a professor even though he never got a Ph.D. (He had been admitted to a PhD program as a teenage prodigy, but flunked out and never went back.) In that same year, Albert R. Meyer was appointed Assistant Professor in the Carnegie Tech Computer Science Department, where he first met Floyd. Floyd and Meyer were the only theoreticians in the department, and they were both delighted to talk about their shared interests. After just a few conversations, Floyd’s new junior colleague decided that Floyd was the smartest person he had ever met. Naturally, one of the first things Floyd wanted to tell Meyer about was his new, as yet unpublished, Invariant Principle. Floyd explained the result to Meyer, and Meyer wondered (privately) how someone as brilliant as Floyd could be excited by such a trivial observation. Floyd had to show Meyer a bunch of examples before Meyer understood Floyd’s excitement — not at the truth of the utterly obvious Invariant Principle, but rather at the insight that such a simple method could be so widely and easily applied in verifying programs.
- mabbo 8y agoI think what many commenters are missing is why this is important. Invariants like this allow one to prove the correctness of their code. That may not seem like a big deal most of the time, but imagine you're working on a satellite that's going to Jupiter, where a bug in the code could mean 10 years from now a billion dollar project gets scuttled. Imagine you're building subroutines that will go into 10,000 pacemakers next year. Imagine you're writing the navigation logic for a cruise missile. There are many times where proving your code correct is taken very, very seriously. Invariants are a tool to do so more easily.
- deleted 8y ago[deleted]
- ramtatatam 8y agoTo prove the correctness of your code you would write tests in similar way as SQLite does, no? They have, like, 100x more lines of code for tests than actual code they test?
- jacobajit 8y agoTest cases do not establish proof. There could always be another rare edge case.
- heartofgold 8y agoWhat jacobajit said. Or here's what Dijkstra said: "Program testing can be used to show the presence of bugs, but never to show their absence!" Dijkstra (1970)
- mabbo 8y agoUnit tests demonstrate correctness. That's another useful tool in the tool box. But proofs are more than just that. Imagine trying to unit test all possible cases of Pythagorean theorem being correct vs a single proof in a few lines of descriptive logic.
- earthicus 8y agoI don't think the utility of invariants is restricted to proving program correctness, as is suggested by a number of commenters in this thread. Instead, they identify some underlying structure in your problem, and that structure can be exploited to simplify your method of calculation. Another great example of exploiting a (not-really-loop) invariant to design an algorithm is Sean Parent's implementation of a generic 'gather' algorithm, which takes advantage of the fact that the set of objects below/above the gathering point is unchanged, allowing you to split the problem into two easier sub-problems. Here's his explanation and implementation (video should be linked to 16:50): https://youtu.be/IzNtM038JuI?t=1009 https://youtu.be/IzNtM038JuI?t=1009
- mikhailfranco 8y agoEiffel has loop invariants, for example see: http://se.ethz.ch/~meyer/publications/methodology/invariants.pdf http://se.ethz.ch/~meyer/publications/methodology/invariants... Also see Meyer's Design By Contract book, which you should read even if you will never use Eiffel - it's a gem.