ADDRESSING THE SHORTCOMINGS OF TRADITIONAL FORMAL REASONING METHODS FOR CONCURRENT PROGRAMS - NEW TOOLS AND TECHNIQUES FOR SOURCE CODE CORRECTNESS

Using an informal but realistic model, this paper argues that human pr ogrammers reason about their source code on multiple abstraction level s. Distinguishing features of these levels are given. Traditional reas oning methods that use code annotation are analyzed and shown to be in adequate for certain such levels. A new design architecture that expli citly captures the multi-level paradigm is presented along with a prot otype implementation. The prototype demonstrates support for fine-grai ned, highly interactive analysis of source code without requiring form al-methods expertise from the user. (C) 1998 Elsevier Science Inc. All rights reserved.