What is an invariant? (2023)
matklad.github.io61 points by SchwKatze 4 days ago
61 points by SchwKatze 4 days ago
I’m not sure that I agree with the article.
In the course of my work, I think of an invariant as a state that must hold true at all points during the software’s execution.
For example, “port xxx must never accept inbound traffic”.
I don’t think of invariants as mindsets; I think of them as runtime requirements that are observable and testable at any point during execution, and whose violation is an indication that some assumption about state that the proper execution of the software depends on, no longer holds.
Maybe a good analogy would be “a runtime assert”.
CLRS defines loop invariants pretty clearly:
We must show three things about a loop invariant:
Initialization: It is true prior to the first iteration of the loop.
Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration.
Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.
lo <= insertion_point <= hi
should hold on every iteration. It clearly holds before we enter the loop.
[...] The invariant, the condition binding lo and hi, holds on every iteration.
In terms of concrete implementations of an algorithm, this in some way makes the "runtime assert" redundant, for, at least in principle, one can statically analyze the code and then prove, before runtime, that the expressions being asserted must necessarily be true (subject to certain preconditions), and even optimize them out.
Of course, this presumes that you have indeed implemented the algorithm correctly - and one way to determine this is to see whether or not your implementation satisfies those same properties and invariants that the abstract description of the algorithm depends upon, and the article also discusses this point.
> In the course of my work, I think of an invariant as a state that must hold true at all points during the software’s execution.
That seems quite close to the author's answer:
> Perhaps it’s time to answer the title question: invariant is some property which holds at all times during dynamic evolution of the system.
Indeed, but the author works through a deeply idiosyncratic train of thought before getting to that, and then quickly continues with some creative analogizing about how the idea of an invariant might be applied at other scales.
For an essay titled "What is an invariant?", it doesn't really focus on answering the question at all and so the GP's failure to spot the traditional answer is pretty reasonable. A more fitting title may have been something more like "Invariants in software system design" -- better framing that it'll be a survey of examples and their rationales rather than an analysis of invariants.
It's just the inductive reasoning version of the essay rather than the deductive version.
A lot of software exposition fails on that front. If you're familiar with invariants as a crucial tool for reasoning about software systems, then the essay will be a bit fluffy. It looks decent for a newcomer to the topic to rapidly build up intuition though.
For data structures, an invariant is something that must hold true at the end of all its public APIs. For example a doubly-linked list may have to break invariants around its pointers while in the middle of a splice or insert. But at the end of those public routines they must all be valid and conformant to the type’s requirements.
Right. A "system" is the observable parts.
If you have a good wall of abstraction, you have freedom in the internals and security in the observables.
I appreciate that the Ada language features baked-in pre- and post-condition invariants as a part of a function's signature. It goes beyond just runtime assertions by becoming a part of the function's contract with callers.
https://learn.adacore.com/courses/intro-to-ada/chapters/cont...
Another way to view such invariant is to see it as a generalization of both pre- as well as post-condition.
The pre-condition is a special case, then the invariant provides the "guard rails" along which the computation proceeds, and then the post-condition is again a special case which ultimately is the result of the computation.
In the search example of the computation, the pre-condition is "the position is somewhere in the allowed indices", the post-condition is "the return value is the position". The stated invariant is "the value is between current min and max bounds". These bounds become tighter and tighter, so that eventually the pre-condition is transformed into the post-condition.
Perhaps a nice short summary would be "facts you can rely on". Because the benefit comes from reducing the cognitive load juggled by the programmer. The more possibilities you can eliminate by identifying invariants, the quicker you'll arrive at a working solution.
[flagged]