h2smt

This program can parse, and verify hoare proofs of an imp-like language.

Overview

Imp-like programs, annotated with hoare predicates, are parsed into an AST using flex and bison.

The AST is then traversed in accordance with the common hoare rules to verify the correctness of the annotated program.

Hoare triples are translated into SMT formulas, as described here, which are then verified using the Z3 SMT prover. Using this translation scheme, counterexamples to the hoare proof are extracted from the SMT model and presented to the user if the hoare proof turns out to be invalid.

Grammar

The accepted language is as follows:

Aexp → var | int
   | Aexp + Aexp
   | Aexp - Aexp
   | Aexp * Aexp
   | Aexp / Aexp

Bexp → true | false
   | Bexp = Bexp
   | Bexp ≠ Bexp
   | Bexp > Bexp
   | Bexp < Bexp
   | Bexp ≥ Bexp
   | Bexp ≤ Bexp
   | ¬ Bexp
   | Bexp ∧ Bexp
   | Bexp ∨ Bexp
   | Bexp ⇒ Bexp

Command → skip
   | var := Aexp
   | if Bexp then Block else Block
   | while Bexp do WhileBlock

Block → ( { Bexp } Command; )* { Bexp }
WhileBlock → ( Command { Bexp } )* Command

Where

• Aexp represents an arithmetic expression
• Bexp represents a boolean expression
• Command represents an imp-like command
• { Bexp } represents a hoare predicate