Refactoring Functional Programs

[back to project home page]

A small, but growing heap of potentially related work, in no particular order. To be harvested, amended, summarised and sorted..

Program transformation

• A survey of the early work:

          @article{PartschSteinbrueggen83,
            author  = {H.~Partsch and R.~Steinbr{\"u}ggen},
            title   = {Program Transformation Systems},
            journal = {ACM Computing Surveys},
            volume  = 15,
            number  = 3,
            month   = Sep,
            year    = 1983,
            topics  = {Reflection/Meta-Programming}
          }
          

  Also interesting: go to the ACM Digital Library, and enter "program transformation" in the search field.

• The Program Transformation Wiki has a section on transformation systems

• TAS and IsaWin are tools for formal program development and theorem proving developed at the University of Bremen and Albert-Ludwigs-Universität, Freiburg. TAS is a transformation system based on the theorem prover Isabelle. It features transformations based on Isabelle theorems, a graphical user interface based on the principle of direct manipulation; genericity (it can be used for any formal method which offers a notion of correctness-preserving refinement, or in fact any transitive-reflexive transformation relation, which is encoded into Isabelle). We have investigated instantiations for classical program transformations (in the style of systems like KIDS using plain higher-order logic), for the specification language Z (using the HOL-Z encoding), the process calculus CSP (using the HOL-CSP encoding), and the algebraic specification language CASL (using the HOL-CASL encoding). IsaWin is a graphical user interface for the theorem prover Isabelle. It offers the user a more abstract view on Isabelle then its ususal command-line based interface.

• The project PROSPECTRA ("PROgram development by SPECification and TRAnsformation") aimed to provide a rigorous methodology for developing correct software and a comprehensive support system. The results are substantial: a theoretically well-founded methodology covering the whole development cycle, a very high-level specification and transformation language family allowing meta-program development and formalisation of the development process itself, and a prototype development system supporting structure editing, incremental static-semantic checking, interactive, context-sensitive transformation and verification, development of transformation (meta-) programs, version management, etc., with an initial library of some specifications and a sizable collection of implemented transformations. A summary was published as: B. Hoffmann, B. Krieg-Brückner (eds.): Program Development by Specification and Transformation - The PROSPECTRA Methodology, Language Family, and System, LNCS 680, Springer Verlag, 1993.

Tool generators for language-aware environments

• The Centaur system was conceived as a generic interactive environment generator, that, when given the formal specification of a programming language (syntax and semantics), produces a language-specific environment. With the help of Centaur one can develop tools needed for a programming environment: structure editors, debuggers, interpreters, and various translators (for manipulating programs or objects). It is also possible to incorporate existing tools in a Centaur-generated environment. A generic system, Sophtalk, is provided for communication between tools; Centaur itself is multi-process.

• The Synthesizer Generator is a tool for creating language-sensitive editing environments and interfaces (bibliography). Rules input to the Synthesizer Generator define a language's abstract syntax, context-sensitive relationships, display formats, concrete input syntax, and source-to-source restructuring transformations. The Synthesizer Generator then creates an editor for manipulating objects according to the given rules. The treatment of language syntax and static semantics by the Synthesizer Generator is of particular importance. The editor-designer's specification of the language's syntax can address not only context-free syntax but also context-sensitive conditions such as type correctness. As the user creates and modifies objects, the generated editor incrementally checks for violations of specified context conditions.

• Harmonia is an open, extensible framework for constructing interactive, language-aware programming tools.. Harmonia includes an incremental GLR parser (which admits a more natural syntax specification than LR), a static semantic analysis engine, and other language-based facilities. Program source code is represented by annotated abstract syntax trees augmented with non-linguistic material such as whitespace and comments. The analysis engine can support any textual language that has formal syntactic and semantic specifications. The incremental nature of the analysis supports a history mechanism that is used both for history-based diagnostic information and for contextual rollback. Harmonia can be used to augment text editors to robustly support the language-aware editing and navigation of documents, including those that are malformed, incomplete, or inconsistent (i.e. the document can remain in that state indefinitely). We have integrated Harmonia into XEmacs by creating a new Emacs "mode" that provides interactive, on-line services to the end user in the program composition, editing and navigation process. New languages can be easily added to Harmonia by giving the system a syntactic and semantic description, which is compiled into a dynamically loadable extension for that language. Among the languages for which descriptions exist are Java, Cool (a teaching language), XML, Scheme, Cobol, C, and C++. Other languages are being added to Harmonia as resources permit.

A historical note

We all tend to refactor our programs, though we might not recognise the activity. The first to bring the activity to our attention might have been Robert W. Floyd.

@InCollection{Floyd87,
  author =       "Floyd",
  title =        "The Paradigm of Programming (1978)",
  booktitle =    "ACM Turing Award Lectures: The First Twenty Years, ACM
                 Press Anthology Series, ACM Press, New York,
                 Addison-Wesley",
  year =         "1987",
}

If you are aware of other relevant pointers, please send us an email, and we'll eventually get round to updating this page.