Approximate reasoning about the semantic effects of program changes

摘要

It is pointed out that the incremental cost of a change to a program is often disproportionately high because of inadequate means of determining the semantic effects of the change. A practical logical technique for finding the semantic effects of changes through a direct analysis of the program is presented. The programming language features considered include parametrized modules, procedures, and global variables. The logic described is approximate in that weak (conservative) results sometimes are inferred. Isolating the exact effects of a change is undecidable in general. The basis for an approximation is a structural interpretation of the information-flow relationships among program objects. The approximate inference system is concise, abstract, extensible, and decidable, giving it significant advantages over the main alternative formalizations. The authors' implementation of the logic records the justification for each dependency to facilitate the interpretation of results.