Lot'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/1512…
Loop invariants can give you coding superpowers
11–20 of 88 posts
Re: Loop invariants can give you coding superpowers
#12I 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
);
Re: Loop invariants can give you coding superpowers
#13If 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. The official repository is here: 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.
Re: Loop invariants can give you coding superpowers
#14I 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…
I 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.
Re: Loop invariants can give you coding superpowers
#15Is there a list of loop invariants for algorithms that are frequently used in interviews?
Not sure what you mean by your comment. You can use loop invariants when solving problems that call for an iterative solution.
Re: Loop invariants can give you coding superpowers
#16I 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…
You 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.
Re: Loop invariants can give you coding superpowers
#17The 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.
Re: Loop invariants can give you coding superpowers
#18I 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,...)
Re: Loop invariants can give you coding superpowers
#19The 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.
How would write an assert for the sum loop invariant?
Re: Loop invariants can give you coding superpowers
#20Interesting 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.
On 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.