Loops in Frml

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 visitor plus the logic that turns a loop into obligations. visit_StmtWhile checks four things: the loop condition must have type Bool, every invariant must have type Bool, the decreases expression when present must have type Int, and the loop body is type-checked in a fresh scope. def visit_StmtWhile(self, stmt, ret): self.check_expr(stmt.cond, expected=BOOL, allow_old=False, result_type=None) self.in_spec = True try: for inv in stmt.invariants: self.check_expr(inv,…