Method and apparatus for automatically inferring annotations

#This application is related to concurrently filed U.S. patent application, Ser. No. 10/007,113, entitled “Method and Apparatus for Automatically Inferring Annotations for an Extended Static Checker,” incorporated herein by reference.

#The present invention relates generally to program checking tools that automatically verify, using static checking techniques, the correctness of a computer program with respect to predefined criteria, and particularly to an inference system that automatically annotates the computer program by iterative application of the program checking tool so as to eliminate or reduce spurious warning messages produced by the program checking tool.

#The purpose of a program checking tool is to analyze a given computer program to determine whether or not it has certain desirable properties. Program checking tools, often called program checkers, are specific examples of verification systems that can also be used to analyze hardware components, formulae, algorithms, or, more generally, behavioral designs.

#Additional objects and features of the invention will be more readily apparent from the following detailed description and appended claims when taken in conjunction with the drawings, in which:

#FIG. 1 is a block diagram of a programmed general purpose computer according to an embodiment of the annotation inference system of the present invention.

#FIG. 2 is a flow chart showing the application of the annotation inference system to a computer program in order to generate a modified computer program.

#Referring to FIG. 1, the present invention may be implemented using a programmed general-purpose computer system 100. The computer system 100 includes: (a) one or more data processing units (CPU's) 102; (b) memory 106, which will typically include both high speed random access memory as well as non-volatile memory (such as one or more magnetic disk drives); (c) a user interface 108 which may comprise a keyboard, mouse and/or touch-screen display; (d) a network or other communication interface 110 for communicating with other computers as well as other devices; and (e) one or more communication busses 104 for interconnecting the CPU(s) 102, memory 106, user interface 108, and network interface 110.

#The computer system's memory 106 stores procedures and data, typically including: an operating system 112 for providing basic system services; one or more application programs 114, such as user level programs for viewing and manipulating images; one or more authoring tools 116, for assisting with the writing of computer programs; a computer program 118 possibly containing some annotations, to be analyzed by an annotation inference system 130; a modified computer program 120 that is the product of applying annotation inference system 130 to computer program 118; and a program checking tool 122 that, when applied to a computer program 118, produces zero or more warnings.

#The annotation inference system 130 preferably includes: an annotation inference module 132, also called an annotation assistant, which is the main procedure of the annotation inference system and controls its overall operation; and a program checking tool 150 that, when applied to a computer program 118, produces zero or more warnings.