|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
 ABSTRACT
Ten years ago Cheatham and Wegbreit [4] proposed a transformational program development methodology based on notions of top-down stepwise program refinement first expressed by Dijkstra [10] and Wirth [45]. A schema describing the process of this methodology is given in fig. 1. To develop a program by transformation, we first specify the program in as high a level of abstraction and as great a degree of clarity as our programming language admits. This high level problem statement program P is proved correct semimechanically according to some standard approach (see Flovd and Hoare [15, 21]), Next, using an interactive system equipped with a library of encoded transformations, each of which maps a correct program into another equivalent program, we select and apply transformations one at a time to successive versions of the program until we obtain a concrete, low level, effecient implementation version P'. The goals of transformational programming are to reduce programming labor, improve program reliability, and upgrade program performance. In order for labor to be reduced, the effort required to obtain P, prove it correct, and derive P' by transformation should be less than the effort required to code P from scratch, and also to debug it. Program reliability will be improved if P can be certified correct, and if each transformation preserves program meaning. Finally, program performance will be upgraded if transformations are directed towards increased efficiency. Experimental transformational systems that emphasize one or more aspects of the methodology outlined above have been implemented by Cheatham [5], Darlington [3], Loveman [27], Standish [41], Feather [14] Huet and Lang [11], and others. However, all of these systems fall short of the goals, because of a number of reasons that include, 1 inability to mechanize the checking of transformation applicability conditions 2 reliance on large, unmanageable collections of low level transformations, and long arduous derivation sequences 3 dependency on transformations whose potential for improving program performance is unpredictable 4 use of source languages insufficiently high level to accommodate perspicuous initial program specifications and powerful algorithmic transformations Yet, convincing evidence that this new methodology will succeed has come from recent advances in verification, program transformations, syntax directed editting systems, and high level languages. These advances, discussed below, represent partial solution to the problems stated above, and could eventually be integrated into a single system 1 The transformational approach to verification was pioneered by Gerhart [19] and strengthened by the results of Schwartz [39], Scherlis [36], Broy et al [2], Koenig and Paige [26.31] Blaustein [1], and others. Due mainly to improved technology for the mechanization of proofs of enabling conditions that justify application of transformations, this approach is now at a point where it can be effectively used in a system. Such mechanization depends strongly on program analysis, and, in particular, on reanalyses after a program is modified. Attribute grammars [24] have been shown to be especially useful in facilitating program analysis [23]. Moreover, Reps [34] has discovered algorithm that reevaluates attributes in optimal time after a program undergoes syntax directed editing changes (as are allowed on the Cornell Synthesizer [43]). He has implemented his algorithm recently, and has reported initial success 2 There are encouraging indications that a transformational system can be made to depend mainly on a small but powerful collection of transformations applied top-down fashion to programs specified at various levels of abstraction from logic down to assembler. We envision such a system as a fairly conventional semiautomatic compiler which classes of transformations are selected semimechanically in a predetermined order, and are justified by predicates supplied mechanically but proved semimanually. Of particular importance is nondeterminism removal which has formulated by Sharir [40] could lead to a technique for turning naive, nondeterministic programs into deterministic programs with emergent strategies. Such programs could then be transformed automatically by finite differencing [13, 16, 17, 18, 29, 30, 31] and jamming [28, 31, 20] (which we have implemented) into programs whose data access paths are fully determined. The SETL optimizer could improve these programs further by automatically choosing efficient data structure representations and aggregations 3 Of fundamental importance to the transformations just mentioned is the fact that they can be associated with speedup predictions Fong and Ullman [16] were the first to characterize an important class of algorithmic differencing transformations in terms of accurate asymptotic speedup predictions, eg, they gave conditions under which repeated calculation of a set former {x in s|k(x)} could be computed on O(#s) + cost(k) steps. By considering stronger conditions and special cases for the boolean valued subpart k, Paige [31] later gave sharper speedup predictions (eg, either O(1) steps for each encounter of the set former or a cumulative cost of O(#s) steps for every encounter) associated with another differencing method. Both Morgenstern [28] and Paige [31] prove constant factor improvements due to their jamming transformations (implemented by Morgenstern for the improvement of file processing, and by Paige for the optimization of programs). Constant factor speedup has also been observed for data structure selection by the method of basings but a supporting analytic study has not been presented [8, 37] 4 Essential to the whole transformational process is a wide spectrum programming language (or set of languages) that can express a program at every stage of development from the initial abstract specification down to its concrete implementation realization. Since transformations applied to programs written at the highest levels of abstraction are likely to make the most fundamental algorithmic changes, it is important to stress abstract features in our language. In addition to supporting transformations, the highest level language dictions should support lucid initial specifications, verification, and even program analysts. Of special importance is SETL [38, 9], because its abstract set theoretic dictions can model data structures and algorithms easily, because its philosophy of avoiding hidden a symptotic costs facilitates program analysis, because its semantics conforms to finite set theory and can accommodate a set theoretic program logic, and because it is wide spectrum. As is evidenced by the work of Schwartz, Fong, Paige, and Sharir, SETL is also a rich medium for transformation. REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage Privacy Policy Code of Ethics Contact Us Useful downloads:  Adobe Acrobat
 QuickTime
 Windows Media Player
 Real Player
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Pdf