Contracts in Frml

The first post in this series introduced Frml, a little procedural language I created so that I could learn how program verification works. The second explained how Frml checks simple scalar code; this one explains how it checks programs with multiple functions. As a reminder, the scalar prover owns the engine and leaves two hooks for higher levels: def verify_function(self, fn): state = State() for p in fn.params: state.vars[p.name] = self._fresh_scalar(p.type, p.name) self._assume_spec(fn, state) end_states = self.exec_stmt_seq(fn.body, state) if fn.return_type is not None: if end_states: raise FrmlVerificationError(...) else: for s in end_states: self._check_ensures(fn, s, None) _assume_spec and _check_ensures do nothing at the scalar level; the contracts prover overrides them: class Prover(ScalarProver): def _assume_spec(self, fn, state): for req in fn.requires: state.path.append(self.eval_expr(req, state)) if fn.decreases is not None: d = self.eval_expr(fn.decreases, state)…