Automatic Verification of Textbook Programs that Use Comprehensions

Textbooks on program verification make use of simple programs in mathematical domains as illustrative examples. Mechanical verification tools can give students a quicker way to learn, because the feedback cycle can be reduced from days (waiting for hand-proofs to be graded by the teaching assistant) to seconds or minutes (waiting for the tool’s output). However, the mathematical domains that are so familiar to students (for example, sum-comprehensions) are not directly supported by first-order SMT solvers.

This paper presents a technique for translating common comprehension expressions (sum, count, product , min, and max) into verification conditions that can be tackled by two first-order SMT solvers. The technique has been implemented in the Spec# program verifier. The paper also reports on the experience of using Spec# to verify several challenging programming examples drawn from a textbook by Dijkstra and Feijen.