Specifications from source code-alchemists´ dream or practical reality?

The author describes the application of formal program transformations to uncover specifications from source code. He takes as an example a small report writing program. Due to errors in the original design, this program had several bugs which were gradually uncovered and fixed in the usual way. The resulting program appears to work, but has a complex and messy structure which makes it extremely difficult to maintain. The aim of the case study is to restructure the program and extract its specification (a concise, high-level description of what the program does which ignores the low-level details of how this result is achieved). It should be noted that his aim is emphatically not that of design recovery in the sense of recovering the original design. Instead he aims to transform the base metal of unstructured code into the gold of a high-level specification. The approach is based on a Wide Spectrum Language (called WSL) which includes both high level abstract specifications and low-level programming constructs within the same language