J. Darlington. A Synthesis of Several Sorting Algorithms. Acta Informatica, 11:1--30, 1978.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....Theorem proving systems became much more able to handle mathematical induction and subsequently Manna and Waldinger [MW80] again integrated their techniques with a theorem prover. The FUM presented by Burstall and Darlington [BD77] was designed as functional program transformation system. In [Dar78] Darlington shows how the same rules can be used for program synthesis. The practical aspects of Burstall and Darlington s system are described in [Dar81] Barstow [Bar77] presented a system for synthesising LISP programs from speci cations using a knowledge based approach. The system re nes ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1-30, 1978.

....guration is generated, and thus eciency is improved. By applying our proposed list introduction strategy we will mechanically derive a program which is similar to the accumulator program version of [StS94] Indeed, this strategy will allow us to realise the so called lter promotion described in [Bir84, Dar78], by which the safeness test is promoted into the generation process and the number of generated unsafe board con gurations is decreased. A similar e ect may also be achieved by the compiling control technique described in [BDK89] which works by transforming a given initial program into a new ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1-30, 1978.

....guration is generated, and thus, eciency is improved. By applying our proposed list introduction strategy we will mechanically derive a program which is similar to the accumulator program version of [StS94] Indeed, this strategy will allow us to realize the so called lter promotion described in [Bir84, Dar78], by which the safeness test is promoted into the generation process and the number of generated unsafe board con gurations is decreased. A similar e ect may also be achieved by the compiling control technique described in [BDK89] which works by transforming a given initial program into a new ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1-30, 1978.

....representation scheme such as [Bobrow77] while the formal model approach uses a mathematical language such as predicate calculus. These two approaches can be contrasted by comparing two works which synthesize sorting routines. The knowledge based approach is characterized by [Green77] while [Darlington78] represents the formal model approach. Knowledge Based Automatic Programming Knowledge based automatic programming originated with experiments with compiling techniques [Simon63] After a long dormancy, it was revived by work on robot planning such as [Sussman73] where the emphasis was on the ....

.... have arisen to verify the correctness of a transformation [Gerhardt75, Neighbors78] The general power of transformation systems and their limitations was investigated by Kibler [Kibler78] A criticism of the naive view of developing programs from a simple specification of the problem, as used in [Darlington78], and refining the simple specification into an efficient implementation is made by Dijkstra [Dijkstra77] The criticism is made from the author s view that programs built on an underlying mathematical theory are not amenable to the transformation approach unless quite a bit of mathematical ....

Darlington, J., A Synthesis of Several Sorting Algorithms, ACTA Informatica, 11(1):1-30, 1978.

....of developing a taxonomy was inspired by the method described by Jonkers [Jon83] There it is applied to develop a taxonomy of garbage collection algorithms. The method is also applied to attribute evaluation algorithms by Marcelis [Mar90] Other examples of algorithm taxonomies are found in [Bro83, Dar78]. All algorithms are presented in a somewhat extended version of the guarded command language of Dijkstra [Dij76] in order to avoid the peculiarities of any particular programming language. The algorithms use string type variables in order to abstract from any implementation detail like, for ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1--30, 1978.

....control technique one can improve generate and test programs by simulating a computation rule which selects test predicates as soon as the relevant data become available. A similar idea has also been investigated in the area of functional programming, within the so called lter promotion strategy [9, 46]. Some other transformation techniques for improving generate and test logic programs which are closely related to the compiling control technique and the lter promotion strategy, can be found in [23, 136] The problem of compiling a given computation rule C can be described as follows: given ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:130, 1978.

....lazily. Now that there is an intuitive explanation of the Hopcroft Tarjan algorithm it needs formalising. One particular future project would involve the implementation and calculation of graph algorithms of the three different types. It may be possible to arrive at a similar work to Darlington s [12]. A full implementation of Hopcroft and Tarjan s algorithm in King and Launchbury s style should be attempted and its time complexity at least found. We note that there is no calculus for space usage nor is it likely for some time because this is the most compiler dependent aspect of functional ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1--30, 1978.

....as expected, all of the program except the program points 4 and 5 . 5 Related work The fold unfold transformation framework used here is based on seminal work by Burstall and Darlington [2, 6] The application of the technique to the derivation of programs has also been investigated in [5], which presents the synthesis of several sorting algorithms. The initial specication is expressed in terms of sets and predicate logic constructs. Our transformations are also reminiscent of the deforestation technique [3, 9, 27] in both cases the goal is to transform a composition of recursive ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:130, 1978.

....proof of sort will require induction and this will cause sort to be defined recursively: the form of induction determining the form of recursion. Different proofs of the theorem will synthesise different algorithms for the same function, e.g. bubble sort, merge sort, quick sort, etc (see [ Darlington, 1978] for a detailed discussion) The Automation of Proof by Mathematical Induction 37 Synthesis of recursively defined software, hardware, etc is an important application of inductive theorem proving. So it is important that inductive theorem proving techniques can handle existential variables, in ....

Darlington, J. (1978). A synthesis of several sorting algorithms. Acta Informatica, 11:1--30.

....works in transformational programming. We wanted to consider the problem of sorting, in the context of the calculus, and thereby explore its applicability to the derivation of several sorting algorithms, bearing in mind that these can be viewed as a family descending from a common specification ([Dar78], Zol90] We present here the first step undertaken: the derivation of a sorting algorithm. As a starting point we took a high level specification and transformed it, using the semantics preserving rules of the calculus, until an efficient algorithm was obtained. At some point of the derivation ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1--30, 1978.

....control technique one can improve generate and test programs by simulating a computation rule which selects test predicates as soon as the relevant data are available. A similar idea has also been investigated in the area of functional programming, within the so called filter promotion strategy [ Darlington, 1978; Bird, 1984 ] Some other transformation techniques for improving generateand test logic programs which are closely related to the compiling control technique and the filter promotion strategy, can be found in [ Seki and Furukawa, 1987; Brough and Hogger, 1991; Traff and Prestwich, 1992 ] The ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1--30, 1978.

....(like second order type theory) but others are directly depending on the theory and its characteristics (like second order quantification) 10] 3. 3 Proof and program derivation A good example of program synthesis is the derivation of the well known sorting algorithms from a common specification [6]. We can see how algorithmic features can be reflected in proof strategy to derive proof of formal specification. At first, we present a general formulation of sorting in a mathematical notation and two different strategies of proofs. At the end, it will be important to formulate such expressions ....

J. Darlington. Synthesis of several sorting algorithms. Acta Informatica, 11:1--30, 1978.

....Sort Insertion Sort by insertion Shell Sort Heapsort Merge Figure 1: The traditional taxonomy of sorting algorithms. 2 The Inverted Taxonomy of Sorting Algorithms The alternative taxonomy proposed in (Merritt 1985) was inspired by the work in program synthesis in (Clark and Darlington 1980) (Darlington 1978), Green and Barstow 1978) and (Barstow 1980) The basis of this classification is to recognize sorting as a split and join procedure: given a set of things to sort, split the set into two parts; recursively sort each part; and finally join the two parts into a sorted set. Such a description ....

Darlington, J., (1978), A Synthesis of Several Sorting Algorithms, Acta Informatica, Vol. 11, pp. 1--30.

....disjunctive trees just as they are found in its argument, normalising them into ordered chains of literals enables us to bring forward some of the work from unicl so that heavy pruning can occur earlier in the pipeline. This sort of program transformation is sometimes termed lter promotion[Dar78]. To implement the idea we de ne a normalising constructor dis to be used in place of Dis in the nal disin equation. To realise the full bene ts we also need an extra Formula constructor Taut to represent a tautology. Figure 15 shows how dis is de ned in Version 6 of the clausify program. The ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:130, 1978.

....D) else ( S1 [ S2 [ f g; N1 ) Fig. 6. Dynamic (on the fly) slicing analysis 5 Related work The fold unfold transformation framework used here is based on seminal work by Burstall and Darlington [2, 6] The application of the technique to the derivation of programs has also been investigated in [5], which presents the synthesis of several sorting algorithms. The initial specification is expressed in terms of sets and predicate logic constructs. Our transformations are also reminiscent of the deforestation technique [3, 9, 28] in both cases the goal is to transform a composition of ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1--30, 1978.

.... By applying our proposed transformation technique we will mechanically derive a program which is similar to the accumulator program version of [16] Indeed, the use of list introduction, tupling, and generalization, will allow us to realize the so called lter promotion strategy described in [9] and [2] by which the safeness test is promoted into the generation process and the number of generated unsafe board con gurations is decreased. A similar e ect may also be achieved by the compiling control technique described in [4] which works by transforming a given initial program into a ....

J. Darlington, \A synthesis of several sorting algorithms," Acta Informatica, vol. 11, pp. 1{ 30, 1978.

....disjunctive trees just as they are found in its argument, normalising them into ordered chains of literals enables us to bring forward some of the work from unicl so that heavy pruning can occur earlier in the pipeline. This sort of program transformation is sometimes termed filter promotion[Dar78]. To implement the idea we define a normalising constructor dis to be used in place of Dis in the final disin equation. To realise the full benefits we also need an extra Formula constructor Taut to represent a tautology. Figure 15 shows how dis is defined in Version 6 of the clausify program. ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1--30, 1978.

....the importance of adapted inference rules (leading to tactics) in such theories. 3.3 Examples of proof derivations A good example of synthesis is the derivation of the well known sorting algorithms from a common speci cation. We have some results of such exercise using transformation techniques [5]. Here we want to take up this example in a programming with proofs context with a view to de ning new formulations or extensions to derive eOEcient programs. With the two following examples, we can see how algorithmic features can be reAEected in proof strategy to derive proof of formal ....

....(x ) x.y. a:y,b:x) we obtain the merge sort. Remark 5.6 To obtain other sorting algorithms we have to change the auxiliairy functions that x the style of the derivation. It corresponds to de ning new lter functions for the synthesis [5]. What is not clear is the way to automatize derivations using these new lters. Moreover, to derive for instance the quicksort, a method can be to derive it from equations using the listcases constant. What can we say about eOEciency of quicksort in type theory The questions dealing with ....

J. Darlington. Synthesis of several sorting algorithms. Acta Informatica, 11:1 30, 1978.

....based on their formal construction, or synthesis. In this short paper, we first briefly survey previous work in the synthesis and classification of sorting algorithms. Then we outline our own work in this area, and finally compare our results with the others. 2 Brief Survey of Previous Work In [5], Darlington presents a family tree of six sorting algorithms, as shown in Figure 1. This tree represents a synthesis of these algorithms by program transformation on recursion equations, the key transformation rule being the fold unfold rule of Burstall Darlington [3] and Manna Waldinger ....

Darlington, J.: A Synthesis of Several Sorting Algorithms. Acta Informatica 11, 1-30(1978)

....of the most notable is Broy s sorting algorithm taxonomy [Bro83] In this taxonomy, algorithm and problem details are also added, starting with a naive solution; the taxonomy arrives at all of the well known sorting algorithms. A similar taxonomy (which predates the one of Broy) is by Darlington [Dar78]; this taxonomy also considers sorting algorithms. Our particular incarnation of the method of developing a taxonomy was developed in the thesis of Jonkers [Jon82] where it was used to give a taxonomy of garbage collection algorithms. Jonkers method was then successfully applied to attribute ....

Darlington, J. A synthesis of several sorting algorithms. Acta Informatica, 11 (1978) 1--30.

....has been applied to the derivation of algorithms from their specifications. The main advantage of this approach is that correctness is usually automatically built in. Several people have chosen sorting algorithms for such exercises using different notations and methodologies. 12] Darlington[5] has derived a family of six sorting algorithms, namely quick sort , selection sort , merge sort , insertion sort , bubble sort , and sinking sort . Note that he actually calls bubble sort and sinking sort respectively exchange sort and bubble sort . Our nomenclature shall conform to standard ....

J. Darlington, A Synthesis of Several Sorting Algorithms, Acta Informatica 11(1), 1-30 (1978).

....equations by applying sequences of foldings and unfoldings together with instantiations. In more recent work Darlington has manually derived a cross section of sorting algorithms with an eye to eventually being able to automatically generate the more efficient versions from the remainder ( cf. Darlington [1978] and Darlington [1981] There are many steps in their derivations which clearly involve human ingenuity, or, at least, for which no mechanical explanation is provided. Furthermore, as with their more general program transformation model, Darlington and Burstall are not concerned with the ....

: J. Darlington. A Synthesis of Several Sorting Algorithms. Acta Informatica 11 (1978).

.... Iteration on Darlington s A Synthesis of Several Sorting Algorithms Brian Howard Kansas State University Draft: October 18, 1994 In A Synthesis of Several Sorting Algorithms [Dar78], Darlington showed how to use program transformation techniques to develop versions of six well known sorting algorithms. By systematically constructing these algorithms from a common high level specification he wished to expose the underlying relationships among the algorithms and provide an ....

....into two sublists satisfying the Lowers predicate. Related Work Clark and Darlington [CD80] updated Darlington s original paper to obtain a cleaner derivation (not relying on the original s generate and test approach, nor on a specific coding of sequences as sets; that the derivations in [Dar78] were not simple is supported by another follow up paper in Acta Informatica [JF88] where Jacobs and Feather corrected two errors in the derivation of Quick Sort) of the four sorting algorithms under consideration, and implicitly recognized the fourfold symmetry pointed out by Barstow in [Bar80] ....

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11:1--30, 1978.

No context found.

J. Darlington. A Synthesis of Several Sorting Algorithms. Acta Informatica, 11:1--30, 1978.

No context found.

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11(1):1--30, 1978.

No context found.

J. Darlington. A synthesis of several sorting algorithms. Acta Informatica, 11(1):1--30, 1978.

No context found.

J. Darlington, "A synthesis of several sorting algorithms", Acta Informatica 11, pp. 1-30 (1978).

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.