``Bagatelle in C arranged for VDM SoLo''
[ DI/UM ]

In Journal of Universal Computer Science, 7(8):754-781, 2001.
Special Issue on Formal Aspects of Software Engineering (Colloquium in Honor of Peter Lucas , Institute for Software Technology, Graz University of Technology, May 18-19, 2001). Paper: available from Journal of Universal Computer Science ; Slides: available from the Colloquim web-site.

Abstract: This paper sketches a reverse engineering discipline which combines formal and semi-formal methods. Central to the former is denotational semantics, expressed in the ISO/IEC 13817-1 standard specification language (VDM-SL). This is strengthened with algebra of programming, which is applied in «reverse order» so as to reconstruct formal specifications from legacy code. The latter include code slicing, a «shortcut» which trims down the complexity of handling the formal semantics of all program variables at the same time.

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

The approach is illustrated for a small piece of code already studied in the code-slicing literature: Kernighan and Richtie's word count C programming «bagatelle».

BibTeX:

@article{Ol01b,
   key = "Ol01b",
  author = {J. N. Oliveira},
   title = {``Bagatelle in C arranged for VDM SoLo''
           },
   journal = {Journal of Universal Computer Science},
   volume = "7",
   number = "8",
   pages = "754-781",
   publisher = "Springer Pub. Co.",
   year = "2001",
}