2 ms·
Here's one example that comes to mind. https://queue.acm.org/detail.cfm?id=2038036 https://queue.acm.org/detail.cfm?id=2038036 As you can see, a number of inv
by chubot 8y ago
Here's one example that comes to mind.
https://queue.acm.org/detail.cfm?id=2038036 https://queue.acm.org/detail.cfm?id=2038036
As you can see, a number of invariants tie the different record fields together. Maintaining such invariants takes real work. You need to document them carefully so you don't trip over them later; you need to write tests to verify the invariants; and you must exercise continuing caution not to break the invariants as the code evolves.
It's also covered here under "make illegal states unrepresentable".
https://blog.janestreet.com/effective-ml-revisited/ https://blog.janestreet.com/effective-ml-revisited/
The author is advocating OCaml, which allows you to encode such invariants in the type system.
But 99% of state machines are not written in OCaml -- more often it's C or C++. For example, the entire Linux kernel :-/ So basically I'm saying rather than poking and prodding at the code with the debugger and flipping variables, you can think of your whole program as a state machine, and the state machine has invariants like the ones listed:
last_ping_time and last_ping_id are intended to be used as part of a keep-alive protocol. Note that either both of those fields should be present, or neither of them should. Also, they should be present only when state is Connected.
----
For another example, the "lossless syntax tree" data structure I use for my shell has a number of invariants:
http://www.oilshell.org/blog/2017/02/11.html http://www.oilshell.org/blog/2017/02/11.html
I use the same data structure for generating errors and translating between two languages. So it really has to have some higher-level properties rather than just setting and getting variables.
In C# they have something called "Red-Green Trees" that are similar:
https://github.com/oilshell/oil/wiki/Lossless-Syntax-Tree-Pattern https://github.com/oilshell/oil/wiki/Lossless-Syntax-Tree-Pa...
In summary, your debugger is not going to show you which nodes are red and green in this sense! It has no idea about such things. IMO it's better to think at a higher level when you can.
(Note that red-green trees are just a name for an application-specific concept they made up. I t has nothing to do with red-black trees, which are a generic data structure. Even so, your debugger also has no idea about the invariants in a red-black tree implementation either!)
----
Maybe a simpler way to put it:
- the assert() statement in C and Python checks invariants at runtime. There's something of an art to doing this; I think it's covered in books like "Code Complete". You can grep a codebase for assert() and see what invariants the author wants to maintain.
- I'm not sure if they still teach "loop invariants" anymore, but it basically means "something that's true at every iteration of the loop", regardless of whether it's the first iteration, last one, in the middle, etc. If you have off-by-one errors and you stick in a -1 to fix it, that's a sign that you could think more rigorously about the loop.)
Invariant means "a thing that's always true, regardless of the values of the variables." It's a higher-level property than what the debugger shows you.