by SchwKatze on 1/9/25, 12:24 AM with 14 comments
by efitz on 1/12/25, 2:05 PM
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”.
by driggs on 1/12/25, 8:03 PM
https://learn.adacore.com/courses/intro-to-ada/chapters/cont...
by MarkLowenstein on 1/12/25, 6:32 PM
by fishstock25 on 1/12/25, 8:01 PM
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.
by UltraSane on 1/13/25, 8:11 PM
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()