The first three posts in this series introduced Frml, then explained how it checks simplar scalar code and contracts between functions. This post shows how Frml handles while loops with invariants and termination measures. What It Does Here’s a minimal program with a loop: fn main() -> Int { let i: Int = 0; while i < 3 invariant 0 <= i invariant i <= 3 decreases 3 - i { i = i + 1; } return i; } The loop type checker adds one visitor to the existing code called visit_StmtWhile, and the loop prover adds the same...