Comprehension by derivation [software system comprehension]

We argue that to comprehend a software system is to have a handle on its requirements, specifications, and design decisions. These kinds of information support the reuse of system code for a variety of purposes and support its ongoing extension, migration, and evolution. Our work at Kestrel Institute has focused on ways to mechanize the development and evolution of software from formal specifications. By-products of such a process include formal records of design decisions and proofs, as well as executable code. In this approach, reuse can take place at non-code levels, including domain theories, specifications, and design knowledge. Evolution takes place by modifying requirements, specifications, or design decisions, and then reusing previous design structures. When restricted to particular application domains, the generation of correct-by-construction code from specifications can be completely automatic.