9. The digital computer system of claim 1 further comprising a monitor for displaying code undergoing analysis, said monitor including a first display window for displaying a select portion of source code and a second display window for displaying select IL statements corresponding to said select portion of source code.
1. A digital computer system comprising: translating means for translating a source code file into an intermediate language (IL) file, wherein said IL file includes a plurality of IL statements; a memory unit, coupled to said translating means, for holding said source code file and IL file, each of said plurality of IL statements being maintained in a data structure providing a connectivity to neighboring IL statements; a user interface, coupled to said translating means, for selecting a starting point at a first IL statement and an ending point at a second IL statement thereby defining a portion of said IL file; and analysis means, coupled to said user interface, for analyzing said portion of said IL file by traversing said portion in forward executable order pursuant to said connectivity to identify a plurality of paths, and by subsequently traversing said plurality of paths in reverse executable order pursuant to said connectivity to generate a plurality of weakest preconditions for said plurality of paths, wherein said plurality of weakest preconditions are combined to form a single weakest precondition of said portion.