Scalar Code 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. This post explains how Frml checks scalar-level programs that have straight-line and branching code over scalar values with no function calls, contracts, loops, or quantifiers. The Prover’s Data Model The prover tracks a program point with a State object. State.vars holds the symbolic values of scalar variables, and State.path holds every fact assumed to hold so far. The prover never stores concrete numbers in variables; it stores Z3 formulas about numbers. For example, x might hold the symbolic integer x!1 rather than the number 5, where x!1 means “the first fresh symbol named x”. An Obligation records one claim to prove. Its kind can be assert or division at this level, its description is the human readable text of the claim, hyp is the list of hypothesis terms, goal is the goal term, and pos is the source position of the claim (shown in --trace…