Algorithm Explanation: Visualizing Abstract States and Invariants

摘要

Software visualization provides methods to facilitate the understanding of algorithms and programs. Practically all existing visualization systems actually execute the code to be visualized on sample input data. In this paper, we propose a novel approach to algorithm explanation based on static program analysis, specifically shape analysis. Shape analysis of a program operating on heap-based data structures analyzes the program to find out relevant properties of its heap contents. The shape analysis we are using is parameterized with sets of observation properties, which are relevant properties of heap elements. Shape analysis associates sets of shape graphs with program points. These graphs describe both structural properties and non-structural properties such as sortedness. By summarizing sets of undistinguishable heap cells shape analysis supports focusing on active parts of the data structure. By computing the program's invariants it provides the basis for their visualization. After the application of the shape analysis the program is visually abstractly executed, i.e., traversed with a strategy corresponding to a meaningful explanation. Showing a sequence of shape graphs produced along a program path demonstrates how invariants are temporarily violated and then restored.