4 ms·
The 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 t
by GuiA 8y ago
The 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.