Computer science students often evaluate the behavior of the code they write by running it on specific inputs and studying the outputs, and then apply their comprehension to a more general understanding of the code. While this is a good starting point in the student’s career, successful graduates must be able to reason analytically about the code they create or encounter. They must be able to reason about the behavior of the code on arbitrary inputs, without running the code. Abstraction is central for such reasoning.

In our quest to help students learn to reason abstractly and develop logically correct code, we have developed tools that rely on a verification engine. Code involves assignment, conditional, and loop statements, along with objects and operations. Reasoning activities involve symbolic reasoning with simple assertions and design-by-contract assertions such as pre-and post-conditions as well as loop invariants with data abstractions. Students progress from tracing and reading code to the design and implementation of code, all relying on abstraction for verification. This paper reports some key results and findings from associated studies spanning several years.