What is an invariant? (2023)(matklad.github.io)

71 pointsby SchwKatze9 days ago6 comments

efitz6 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”.
- ryandv5 days ago
  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.
- JadeNB6 days ago
  > 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.
  - swatcoder6 days ago
    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.
    hansvm6 days ago
    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.
  - MontagFTB6 days ago
    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.
    lupire6 days ago
    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.
- UltraSane4 days ago
  "Maybe a good analogy would be “a runtime assert”."
  The first example if found when googling "python invariants" was a BankAccount class that did exactly this
  class BankAccount:
  """ A bank account class with a representation invariant: balance is always non-negative. """ def __init__(self, initial_balance): self.balance = initial_balance assert self.balance >= 0, "Balance cannot be negative" def deposit(self, amount): assert amount > 0, "Deposit amount must be positive" self.balance += amount def withdraw(self, amount): assert amount > 0, "Withdrawal amount must be positive" assert self.balance >= amount, "Insufficient funds" self.balance -= amount
driggs5 days ago
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...
- UltraSane4 days ago
  Why didn't Ada become as popular as Rust? I think I read that Ada compilers were incredibly expensive.
  - renox4 days ago
    It sure didn't help Ada's beginnings, but I think that there was a free Ada compiler before Rust.
MarkLowenstein5 days ago
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.
fishstock255 days ago
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.

using a SMT solver like Z3 to define and test invariants is a really interesting application of an extremely powerful tool.

from z3 import *

def check_invariant(precondition, loop_body, invariant): """ Check if a loop invariant holds.

    Args:
        precondition (z3.ExprRef): The precondition of the loop.
        loop_body (Callable[[z3.ExprRef], z3.ExprRef]): A function representing the loop body.
        invariant (z3.ExprRef): The loop invariant to check.
    """

    s = Solver()
    s.add(precondition)

    # Check if the invariant holds initially
    s.push()
    s.add(Not(invariant))
    if s.check() == sat:
        print("Invariant does not hold initially.")
        return

    s.pop()

    # Check if the invariant is preserved by the loop body
    s.push()
    s.add(invariant)
    s.add(loop_body(invariant))
    s.add(Not(invariant))
    if s.check() == sat:
        print("Invariant is not preserved by the loop body.")
        return

    s.pop()

    print("Invariant holds.")

# Example: Proving that the sum of the first n integers is n(n+1)/2 def example(): n = Int('n') i = Int('i') sum = Int('sum')
precondition = And(n >= 0, i == 0, sum == 0) loop_body = lambda inv: And(i < n, sum == i * (i + 1) / 2, i == i + 1, sum == sum + i) invariant = sum == i * (i + 1) / 2 check_invariant(precondition, loop_body, invariant)
if __name__ == "__main__": example()

korasaz5 days ago
[flagged]