Dependency Directed Reasoning in the Analysis of Programs which Modify Complex Data Structures

Abstract

REASON is the deductive component of a luger program understanding system called the Programmer's Apprentice [I~ REASON's key features are : (I) Its use of the Truth Maintenance System [2) to record and manipulate the justifications for its deductions, (2) A discipline of explicitly recording control information In a form which may be manipulated by the reasoning system itself and (3) Its goal of producing a a ·common sense· explanation of how a program functions, as opposed to the formal proofs common in verification. One particularly difficult problem which such a system 1nust face is the analysis of program which allow dest~tlve modifications of potentially shared data structures. Our observation is that experienc.cl programmen tend to make simplifying assumptions when analyzing such programs; even if the. usumptions .... found to be r• theJ can be useful in guiding a more eccurate analysis. Thit paper shows how REASON mlmicl this behaYior of expert programmen.