© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Views of Formal Program Development
E.A. Boiten
PhD thesis, University of Nijmegen, Faculty of Mathematics and Informatics, February 1992 Contains cite159,165,162,161,156. ISBN 90-9004747-6.Abstract
A formal specification describes a problem to be solved on a high level - ideally, it specifies what has to be done, but not how. Such descriptive specifications facilitate the derivation of any of the possible solutions, whereas operational specifications suggest only particular ones.
Formal derivations in this framework consist of semantics preserving transformations, i.e. steps that proceed from solutions to the initial specification to other, more defined, more operational, or more efficient ones. Thus, the resulting programs are correct by construction with respect to their initial specifications.
This thesis contains a number of case studies aiming at the exploration of new territories in the area of program specification and transformation.
Chapter 2,"Improving recursive functions by inverting the order of evaluation" gives a comprehensive survey of one particular transformation strategy (a larger conceptual step in a transformational development that can be described at a more abstract level). This strategy for recursive functions entails the derivation of equivalent functions that use in their recursive evaluations the same arguments in an inverted order. This is an important optimization strategy, in particular for tree-like recursive functions, that are often defined in such a way that several function calls need to be evaluated more than once. By evaluating the function in an inverted order, such multiple evaluations are eliminated.
Chapter 3, "Factorization of the factorial", illustrates a number of the transformations in chapter 2, and also demonstrates the state of the art in recursion simplification transformations. Directed by a small set of simple and well-known heuristics, a previously unknown algorithm for computing factorials is derived. Also, a similar development is shown leading to a corresponding program for a simple pipeline architecture.
Chapter 4, "A note on similarity of specifications and reusability of transformational developments", written together with H.A. Partsch , explores the possibilities of reuse of transformational developments. Although it has often been claimed that this could be done fully mechanically, the experience with a number of derivations in this chapter indicates that this claim is somewhat preposterous. Only by describing the transformation steps in a very abstract way (using just natural language) and by considering very general specifications, can the developments be reused. The central concept is similarity, and several definitions of this informal notion are given, each leading to a particular kind of reuse of derivations. Variants of a derivation of linear search lead to several interesting search algorithms, culminating in derivations by reuse of two complicated string matching algorithms.
Chapter 5, "Intersections of sets and bags of extended substructures - a class of problems", generalizes the specification of pattern matching. It describes a class of problems that can be viewed as a generalization of pattern matching problems. The essence of pattern matching is considered to be the intersection of a particular set with a bag (multiset) of extended substructures of a structured object. The set contains the patterns, the extended substructures are possible occurrences, extended with labels that mark their positions in the original object. This leads to the first ideas on an (interesting) theory on (extended) substructures. It is shown how the abstract description of this class of problems lends itself to calculation in a BMF style. Also, clearly exhibiting the basic structure of such problems facilitates connecting them with various solution strategies.
Chapter 6, "Solving a combinatorial problem by transformation of abstract data types", gives an application of techniques from the area of formal program development in a different area, viz. combinatorics. By describing a given combinatorial problem in terms of abstract data types with equivalences, and transforming those data types, a reduction to a known problem is obtained. Abstract data types proved to be a more suitable specification mechanism in this case than context free grammars, since arbitrary equivalences could be introduced on the data types.
Bibtex Record
@phdthesis{169,
author = {E.A. Boiten},
title = {Views of Formal Program Development},
month = {February},
year = {1992},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Contains cite{159,165,162,161,156}. ISBN 90-9004747-6},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1992/169},
school = {University of Nijmegen, Faculty of Mathematics and Informatics},
}