"Bagatelle in C arranged for VDM SoLo"

• Author(s): Oliveira, José Nuno Fonseca
• Date: 2001
• Persistent ID: http://hdl.handle.net/1822/24574
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Reverse engineering; Denotational semantics; Slicing; Algebra of programming
• Document Type: Article
• Language: English

Description

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 pro- gramming, 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 denota- tions 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”.