[HN Gopher] What is an invariant? (2023)
___________________________________________________________________
What is an invariant? (2023)
Author : SchwKatze
Score : 61 points
Date : 2025-01-09 00:24 UTC (3 days ago)
(HTM) web link (matklad.github.io)
(TXT) w3m dump (matklad.github.io)
| efitz wrote:
| 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".
| JadeNB wrote:
| > 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.
| MontagFTB wrote:
| 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.
| lupire wrote:
| 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.
| swatcoder wrote:
| 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.
| hansvm wrote:
| 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.
| ryandv wrote:
| 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.
|
| Which is very much what the article says:
| 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.
|
| They are indeed observable and testable during runtime, but
| beyond just being dependencies on certain subsets of your state
| space, or "runtime asserts," they are properties that _must_
| hold as a necessary consequence of the operation of the
| algorithm. One proves that an invariant is necessarily true in
| the process of demonstrating the correctness of an algorithm.
|
| 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.
| MarkLowenstein wrote:
| 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.
| fishstock25 wrote:
| 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.
| driggs wrote:
| 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...
___________________________________________________________________
(page generated 2025-01-12 23:01 UTC)