A Human-Centric System for Symbolic Reasoning About Code

While testing and tracing on specific input values are useful starting points for students to understand program behavior, ultimately students need to be able to reason rigorously and logically about the correctness of their code on all inputs without having to run the code. Symbolic reasoning is reasoning abstractly about code using arbitrary symbolic input values, as opposed to specific concrete inputs. The overarching goal of this research is to help students learn symbolic reasoning, beginning with code containing simple assertions as a foundation and proceeding to code involving data abstractions and loop invariants. Toward achieving this goal, this research has employed multiple experiments across five years at three institutions: a large, public university, an HBCU (Historically Black Colleges and Universities), and an HSI (Hispanic Serving Institution). A total of 862 students participated across all variations of the study. Interactive, online tools can enhance student learning because they can provide targeted help that would be prohibitively expensive without automation. The research experiments employ two such symbolic reasoning tools that had been developed earlier and a newly designed human-centric reasoning system (HCRS). The HCRS is a first step in building a generalized tutor that achieves a level of resolution necessary to identify difficulties and suggest appropriate interventions. The experiments show the value of tools in pinpointing and classifying difficulties in learning symbolic reasoning, as well as in learning design-by-contract assertions and applying them to develop loop invariants for code involving objects. Statistically significant results include the following. Students are able to learn symbolic reasoning with the aid of instruction and an online tool. Motivation improves student perception and attitude towards symbolic reasoning. Tool usage improves student performance on symbolic reasoning, their explanations of the larger purpose of code segments, and self-efficacy for all subpopulations