PROGRAM DERIVATION WITH VERIFIED TRANSFORMATIONS - A CASE-STUDY

A program development methodology based on verified program transforma tions is described and illustrated through derivations of a high level bisimulation algorithm and an improved minimum-state DFA algorithm. C ertain doubts that were raised about the correctness of an initial pap er-and-pencil derivation of the DFA minimization algorithm were laid t o rest by machine-checked formal proofs of the most difficult derivati onal steps. Although the protracted labor involved in designing and ch ecking these proofs was almost overwhelming, the expense was somewhat offset by a successful reuse of major portions of these proofs. In par ticular, the DFA minimization algorithm is obtained by specializing an d then extending the last step in the derivation of the high level bis imulation algorithm. Our experience suggests that a major focus of fut ure research should be aimed towards improving the technology of machi ne checkable proofs - their construction, presentation, and reuse. Thi s paper demonstrates the importance of such a technology to the verifi cation of programs and program transformations. We believe that the ut ility of transformational systems to program development will ultimate ly rest on a practical program correctness technology. (C) 1996 John W iley & Sons, Inc.