Loop invariants can give you coding superpowers
yourbasic.org
Loop invariants can give you coding superpowers
1–10 of 88 posts
Re: Loop invariants can give you coding superpowers
#2Interesting 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.
Re: Loop invariants can give you coding superpowers
#3This 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/
Re: Loop invariants can give you coding superpowers
#4Interesting 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.
Several static analyzers (like Frama-C [1]) can extract loop invariants and try to prove them, giving you the best of both worlds.
Re: Loop invariants can give you coding superpowers
#5Learned 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.
Re: Loop invariants can give you coding superpowers
#6This 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-curren...
Re: Loop invariants can give you coding superpowers
#7Is there a list of loop invariants for algorithms that are frequently used in interviews?
Re: Loop invariants can give you coding superpowers
#8Lot'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
Re: Loop invariants can give you coding superpowers
#9I 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.
Re: Loop invariants can give you coding superpowers
#10The 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?