Formal reverse calculation supported by code slicing
[ DI/UM ]

In Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE 2001) 2-5 October 2001, Stuttgart, Germany, pages 35-46. IEEE Computer Society, 2001. Paper: [available as a 558k pdf file]

Abstract: This paper sketches a discipline for reverse engineering which combines formal and semi-formal methods. Among the former is the algebra of programming, which we apply in «reverse order» so as to reconstruct formal specifications of legacy code. The latter includes code slicing, used as a means of trimming down the complexity of handling the formal semantics of all program variables at the same time.

A strong point of the approach is its constructive style. Reverse calculations go as far as imploding auxiliary variables, introducing mutual recursion (if applicable) and transforming semantic functions into standard generic programming schemata such as cata/paramorphisms.

We illustrate the approach by reversing a piece of code (from C to HASKELL) already studied in the code-slicing literature: the word-count (wc) program.

BibTeX:

@inproceedings{VO01,
   author = { G. Villavicencio and J.N. Oliveira },
   title = {
        \htmladdnormallink{
                Formal reverse calculation supported by code slicing
        }{
                http://computer.org/proceedings/wcre/1303/1303toc.htm
        }},
  booktitle = {
        Proceedings of the Eighth Working Conference on Reverse Engineering
        (\htmladdnormallink{WCRE 2001}{http://www.reengineer.org/wcre2001/})
        2-5 October 2001, Stuttgart, Germany},
   publisher = {IEEE Computer Society},
   pages     = {35--46},
   year = {2001}
}