D.R. Smith and M.R. Lowry, Algorithm theories and design tactics, Science of Computer Programming, 14(2-3): 305321, 1990.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

.... filtering (i.e. if there is an element satisfying it, then a larger group of elements will satisfy another property Q, which can be used to filter out non solutions) Excellent starting points for exploring the wealth of research work in general algorithm derivation are Chapter 5 of [35] and [44][46]. Deriving algorithms from highly abstract specifications is still a research challenge, however. In practice, most actual generator systems are less ambitious. Stand alone generators (e.g. 5] 11] 17] 24] 31] 42] usually perform algorithmic refinement by using algorithm schemas: generic ....

D.R. Smith and M.R. Lowry, Algorithm theories and design tactics, Science of Computer Programming, 14(2-3): 305321, 1990.

....refinements like theory 2 interpretations ( Smi93b] and implementation steps ( Dim95] Polarity Analysis is better exploited over PO specifications. The idea of a PO specification was originally used to investigate the logical foundations of some design tactics supported in KIDS ([Smi90, SL90]) In [Dim95] PO specifications are employed to support the development of a sound, sufficient formal method for the (semi)automatic construction of implementation steps. Up to date, to our knowledge, the concept of the PO specification lacks a precise formal definition, based on rigorous, ....

....The introduction of formal specifications in computing often employs the use of a Boolean sort as a syntactical representation of the truth values. This is traditional in the algebraic approach to specifications and has occasionally been the case for logical specifications as well (e.g. [Dim95, Smi93a, Smi93b, SL90]) The problems of a loose introduction or treatment of the Boolean sort turned out to be destructive 6 in several cases. In this section we outline an incremental, well founded, introduction of the Boolean sort for the purposes of many sorted first order theory presentations. Our approach ....

[Article contains additional citation context not shown here]

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer programming, 14(2-3):305--321, September 1990.

....of data that could be hidden, i.e. properties or derivations that are valid in any context that includes the accessible data as a module. Potential practical applications in Computer Science include the joint extension of systems development environments [45] and algorithmic design tools [41, 44, 43] so that modularity is improved and more advanced and general refinements are supported. Reasoning by means of (E Dev encapsulations of) uniform schemata may also assist in specifying and developing formal presentations of algorithmic structure via algorithm theories [44] In fact similar methods ....

....design tools [41, 44, 43] so that modularity is improved and more advanced and general refinements are supported. Reasoning by means of (E Dev encapsulations of) uniform schemata may also assist in specifying and developing formal presentations of algorithmic structure via algorithm theories [44]. In fact similar methods are potentially applicable for the presentation and development of several other design abstractions including problem class specifications and software architecture specifications e.g. 48] and [42] ....

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer programming, 14(2-3):305--321, September 1990.

....dev on the basis of the proof calculus for E spec ) But this is out of the scope of this paper and it is in fact a subject of on going research. The pursued practical applications in Computer Science include the joint extension of systems development environments [35] and algorithmic design tools [32, 34, 33] so that more advanced and general manipulations of specification modules are supported. As is explained in Chapters 5 and 6 of [10] and in [11, 13] a Development Workspace can be used as the means of generating a back end development formalism E dev for a given front end specification ....

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer programming, 14(2-3):305--321, September 1990.

.... syntax: One can derive an 8 , 9 free witness : from the deductive proof of a 9 bound formula. The practical applications in Computer Science we intend to pursue, include the joint extension of application software and systems development environments [35] and algorithmic design tools [32, 34, 33] so that more advanced manipulations of specification modules are supported. ....

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer programming, 14(2-3):305--321, September 1990.

....to operate on a higher level of abstraction and must be based on comprehensible formalizations of application domains and programming concepts rather than on low level inferences of the logical calculus. Algorithm design strategies based on schematic solutions for certain classes of algorithms [38] have proved to be suited best for this purpose since they can be formulated almost entirely in programmer s terminology. It has been demonstrated [39] that algorithm schemata do not only lead to a very efficient synthesis process but can also produce competitive algorithms if properly guided. ....

....partial) computable function body:D6 Set(R) form together a program. A program is correct if for each acceptable input it computes the complete set of output values (8x:D. I(x) body(x) fz:R j O(x,z)g) A specification is satisfiable if it can be extended into a correct program. As in [38] we use a formal notation for programs which emphasizes that we interested in computing the set of all solutions of a given problem (assuming that there are finitely many) FUNCTION f(x: D) Set(R) WHERE I(x) RETURNS fz j O(x; z)g j body(x) The name f can be used in the body in order to describe ....

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14(2-3):305--321, 1990.

....are denoted by applicative expressions and it is possible to improve their e ciency by replacing some subexpressions by more e cient, semantically equivalent new subexpressions. These equivalences are stated as theorems in suitable theories. The schemata approach has been followed also in [138] where it is shown how to derive divide and conquer algorithms starting from a divide and conquer schema expressed in terms of abstract functions. The derived algorithms are correct if they are obtained by substituting some concrete functions for the abstract functions and these concrete functions ....

D. R. Smith. The design of divide and conquer algorithms. Science of Computer Programming, 5:3758, 1985.

....formalisms or frameworks, like, for instance, the ones proposed in [Backus 78, Bauer et al. 85, Bird Meertens 87] In those formalisms strategies take the form of theorems and equations which are used to rewrite programs. We could have also considered the case of Pascal like programs [Illsley 88, Smith 85] where strategies resemble more closely the ones often used in Theorem Proving, such as divide and conquer, global search, local search, and pruning. We have considered the transformation rules and strategies in the case of functional languages and then, separately, in the case of logic ....

Smith, D. R.: The Design of Divide and Conquer Algorithms. Science of Computer Programming 5 (1985) 37--58

....and linker to generate an executable program. During the compilation of Opal certain optimizations make use of algebraic properties introduced by type declarations. It is planned to extend this kind of optimizations by employing transformation theories in the compilation process (see e.g. SL90] This extended compilation makes heavy use of algebraic properties and opens the possibility of more elaborate optimizations than realized in existing compilers. The framework sketched in this paper may also serve as a semantical foundation for this concept of extended compilation, which is a ....

Douglas R. Smith and Michael R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14:305--321, 1990.

....but is well suited for massively parallel computation on distributed memory architectures by making efficiently use of the underlying interconnection network to exchange data. 6 Related Work Much attention has been paid to the formal parallelization of DC algorithms. Smith develops a DC theory [Smi85, Smi93] e.g. DC can be treated as a morphism from a decomposition algebra on the input domain to a composition algebra on its output domain. His emphasis is on the development of a DC algorithm, whereas we are interested in its data parallelization on a particular architecture. Thus, our work ....

D.R. Smith. The design of divide-and-conquer algorithms. Science of Computer Programming, 5:37--58, 1985.

....system or body of knowledge is described by a network of theories linked by interpretations. The little theories method is an old idea that has been used in mathematics since the late 1800s and has been advocated in recent years by a number of computer scientists for various purposes (e.g. see [1, 2, 5, 6, 7, 8]) The imps theorem proving system [3] supports the little theories method and contains a large database of traditional mathematics organized as a network of theories. Suppose that an intelligent agent is trying to solve a goal G in a some theory T within a theory network. How can an intelligent ....

D. R. Smith and M. R. Lowry. Algorithmic theories and design tactics. Science of Computer Programming, 14:305-321, 1990.

....1 . This latter sort of re nement is much like a de nition done in reverse. Re nement is a basic technique in computer science for specifying and building computer systems. Theory interpretation is an excellent tool for rigorizing computer system development based on re nement (for examples, see [20, 21, 29, 33, 35]) The interpretation in the next example formalizes the symmetry between left and right multiplication in a monoid. Example 3.2 Let M be the theory consisting of the following three sentences in the rst order language of a binary function constant and an individual constant e: 1. ....

D. R. Smith and M. R. Lowry. Algorithmic theories and design tactics. Science of Computer Programming, 14:305-321, 1990.

....to 8y: var x 6 var y from which we may easily prove the goal. 7.3.8 comment This verification of a unification is another in a long line of such developments. From Zohar Manna and Richard Waldinger s pioneering hand synthesis [MW81] through Lawrence Paulson s machine verification in LCF [Pau85] to the more recent work in diverse proof systems [Coen92, Rou92, Jau97, Bove99] all have faced the same inherent problem of explaining a program which simply does not make the sense its maker intended. 215 Critical to the correctness of the unification algorithm is the relativisation of terms ....

....proof. The choice of this ordering is not so well motivated formally as the other steps of this derivation. The necessary ordering combines lexicographically the size of the variable set and the structure of the problem the different treatments manifest this in slightly different ways. Paulson [Pau85] points out that he works rather harder than he would like to, motivating the desire for an LCF package for well founded induction in order to emulate Manna and Waldinger s paper development more closely. Implementations of what would otherwise be generally recursive programs in type theory ....

Verifying the Unification Algorithm in LCF. Science of Computer Programming, 5:143--169. North-Holland. 1985. 228

....a technique cannot be used generally that we can deduce that it cannot be used very usefully for a whole class of particular cases. 4 Pioneering work in program synthesis among classes of problems has been done mainly by D. Smith. He already studied the following classes: Divideand Conquer [Smi85a, Smi85b, Smi87a] Problem Reduction Generators [Smi91] abstracting general Branch and Bound and Dynamic Programming, Global Search [Smi87b] abstracting bactrack and Branch and Bound and Local Search (hillclimbing) Low91] with M. Lowry (see Appendix) D. Smith inserted those different classes ....

....section, we are going to investigate how it s possible to help a user in the design of a greedy algorithm solving a given formal specification. Our approach will be similar to Smith s one in the way to: ffl characterize the class of Greedy Algorithms as Smith already did for Divide and Conquer [Smi85a, Smi85b, Smi87a] Problem Reduction Generators [Smi91] Global Search [Smi87b] and with Lowry for Local Search (see Appendix) ffl formalize the synthesis process [SL90, Smi92, Smi93] Two interesting consequences of this study would be: 1. to create a framework which could help in ....

D.R. Smith. The design of divide and conquer algorithms. Science of Computer Programming, 5(1):37--58, 1985.

.... to Smith s one in the way to: ffl characterize the class of Greedy Algorithms as Smith already did for Divide and Conquer [Smi85a, Smi85b, Smi87a] Problem Reduction Generators [Smi91] Global Search [Smi87b] and with Lowry for Local Search (see Appendix) ffl formalize the synthesis process [SL90, Smi92, Smi93] Two interesting consequences of this study would be: 1. to create a framework which could help in synthesizing greedy algorithms; 2. to improve Smith s hierarchy of classes [Smi93] by inserting the Greedy Algorithms class and comparing it to some others (see Appendix) A ....

D.R. Smith and M.R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14(2-3):305--321, 1990.

....in Classical Program Transformation In the design of algorithms, certain schemata can be identi ed [7] When such a schema is formalised as a theorem in the form of (6) we call the resulting transformation rule a design transformation. Examples include divide and conquer [20] global search [22] or branch and bound. Recall from Sect. 2.2 that transformation rules are represented by a logical core theorem with an input pattern and an output pattern. Characteristically, design transformations have as input pattern a speci cation, and as output pattern a program. Here, a speci cation is ....

....and interactive proof via IsaWin. Depending on the particular logic, further proof procedures may be at our disposal, such as specialised tactics or model checkers integrated into Isabelle. Another well known scheme in algorithm design is global search which has been investigated formally in [22]. It represents another powerful design transformation which has already been formalised in an earlier version of TAS [13] 4 Process Modelling with CSP This section shows how to instantiate TAS for re nement with CSP [19] and will brie y present an example how the resulting system can be used. ....

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14:305- 321, 1990.

....Design Transformations in Classical Program Transformation In the design of algorithms, certain schemata can be identi ed [7] When such a schema is formalised as a theorem in the form of (6) we call the resulting transformation rule a design transformation. Examples include divide and conquer [20], global search [22] or branch and bound. Recall from Sect. 2.2 that transformation rules are represented by a logical core theorem with an input pattern and an output pattern. Characteristically, design transformations have as input pattern a speci cation, and as output pattern a program. Here, a ....

.... = struct val name = HolRef val trans = ref trans] val refl = ref refl] val weak = val mono = ref if, ref else, ref conj1, ref conj2, ref disj1, ref disj2, val ref conv = end structure TAS = TAS(HolEqTrfThy(HolRefThy) The divide and conquer design transformation [20] implements a program f : X Y by splitting X into two parts: the termination part of f , which can be directly embedded into the codomain Y of f , and the rest, where the values are divided into smaller parts, processed recursively, and reassembled. The core theorem for divide and conquer based ....

D. Smith. The design of divide and conquer algorithms. Science of Computer Programming, 5:37-58, 1985.

....of the generic development steps to specific problems. Transformations of different kind and complexity have been integrated into this framework comprising the whole development process: problem solving strategies encoding general algorithmic paradigms such as global search and divide and conquer [10], transformations for the modification of functional specifications such as transformations from the Bird Meertens formalism like fusion or Horner s rule, transformation steps for optimizing recursive functions [3,8] transformations on the level of procedural programs, and implementations of data ....

Douglas R. Smith and Michael R. Lowry. Algorithm Theories and Design Tactics. Science of Computer Programming, 14(2-3):305--321, 1990. 2

....through which incrementality can be discovered in existing programs written in standard languages. Smith s work in KIDS [Smi90,Smi91] is closely related to this work. KIDS is a 39 semi automatic program development system that aims to derive efficient programs from high level specifications [SL90] as is APTS. Its version of finite differencing was developed for the optimization of its derived functional programs and has two basic operations: abstraction and simplification. Abstraction of a function f adds an extra cache parameter to f . Simplification simplifies the definition of f given ....

Douglas R. Smith and Michael R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14:305--321, 1990.

....concerned with list partitions. Most recent work in this area has been concerned with improving the time complexity of naive dynamic programming solutions, by exploiting special properties of the cost function [12] In programming methodology, our work is very much akin to that of Smith and Lowry [23, 24]. Smith s notion of problem reduction generators is quite similar to the generic algorithm presented here, but his results are more concerned with similarities in the derivation process, and not with a single generic program. There has recently been a surge of interest in polytypic programming. ....

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14:305--321, 1990.

....we want to find a function which satisfies this relation, we have to further refine the enclosing specification. This refinement can be guided by a hierarchy of algorithm theories which are used to impose additional structure on the specification. Details of this process can be found in [Smith 93, Smith and Lowry 90] Algorithm synthesis is one of the creative parts of software development and can be used to construct basic interpretations which can then be composed. Specware aids this by providing a scaffolding which takes care of the mundane details, thus letting the developer identify and focus on the ....

Smith, D. R., and Lowry, M. R. Algorithm theories and design tactics. Science of Computer Programming 14, 2-3 (October 1990), 305--321.

....derivations which cannot Journal of the IGPL, Vol. 4 No. 1, pp. 75 95 1996 c fl IGPL 76 Formal Mathematics for Verifiably Correct Program Synthesis be found automatically. Therefore, less rigorous methods are used when developing strategies. During the last decades many approaches (see e.g. [9, 17, 18, 2, 26]) have been implemented and tested successfully for a number of examples. The KIDS system [26, 29] is believed to be close to the point where it can be used to develop small routine programs. But while the theoretical foundations of these strategies are thoroughly investigated their ....

....for Verifiably Correct Program Synthesis be found automatically. Therefore, less rigorous methods are used when developing strategies. During the last decades many approaches (see e.g. 9, 17, 18, 2, 26] have been implemented and tested successfully for a number of examples. The KIDS system [26, 29] is believed to be close to the point where it can be used to develop small routine programs. But while the theoretical foundations of these strategies are thoroughly investigated their implementations are created ad hoc rather than systematically. It is not clear how the systems reflect these ....

[Article contains additional citation context not shown here]

Douglas R. Smith and Michael R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14(2-3):305--321, October 1990.

....symmetry pointed out by Barstow in [Bar80] The derivations used by Barstow were presented in [GB78] which concentrated on building a knowledge base of techniques for programming. Other derivations which reference Darlington in motivating the choices that lead to the four algorithms include Smith [Smi85a, Smi85b] and Traugott [Tra86] Smith s work is particularly interesting in that it analyzes the recursive phase of divide and conquer algorithms as the application of an appropriate algebra homomorphism, which necessarily preserves the surrounding structure this is the essence of the categorical view ....

D.R. Smith. The design of divide and conquer algorithms. Science of Computer Programming, 5:37--58, 1985.

....architecture, we must relate the behavior of the system to the behavior of the subcomponents independent of the style in which the architecture is implemented. With this goal in mind, we have extended Smith and Lowry s methods for specifying the structure of algorithms using algorithm theories [16, 18] to specify the structure of architectures. An architecture theory constrains the behavior of a system in terms of the behavior of its subcomponents via a collection of axioms. The axiomatic constraints can be used to reason in both a top down and a bottom up manner. Given a system specification, ....

....that must hold between a legal input and a feasible output. A theory based framework can also be used to specify abstract data types [5] providing a direct pathway to extend our ideas to a more complex component model. A component is represented formally as an extension of the problem theory [18] shown in Figure 2(a) A specification for a specific problem is created by a specification morphism from the problem theory that provides definitions for the domain, range, precondition and postcondition. For example, a search problem is specified in Figure 2(b) A component theory 1 extends a ....

[Article contains additional citation context not shown here]

Douglas R. Smith and Micheal R. Lowry. Algorithm Theories and Design Tactics. Science of Computer Programming, 14:305--321, 1990.

....be some traceablity between the system and component level functionality. Therefore, high level architecture specifications should focus on capturing this relationship. With this in mind, we have extended Smith and Lowry s work on using algorithm theories to specify the structure of algorithms [Smi90, SL90, Smi93] to specify the structure of architectures. An architecture theory constrains the behavior of a system in terms of the behavior of its subcomponents via a collection of axioms. These axiomatic constraints can be used in both a top down and a bottom up manner. Given a system specification, an ....

....We required a representation for architectures that relates the operation of the system to the operation of the subcomponents independent of the style in which the architecture is implemented. For this reason, we decided to extended Smith and Lowry s work on specifying the structure of algorithms [Smi90, SL90, Smi93] to specify the structure of architectures. Formal models of architectural style will provide a formal link between an architecture theory and an architecture schema which implements the theory. ....

Douglas R. Smith and Micheal R. Lowry. Algorithm Theories and Design Tactics. Science of Computer Programming, 14:305--321, 1990.

....about this relationship requires an architecture representation that abstracts out the operational details and provides a declarative specification of an architecture. With this in mind, we have extended Smith and Lowry s work on using algorithm theories to specify the structure of algorithms [16, 19] to specify the structure of architectures. An architecture theory constrains the behavior of a system in terms of the behavior of its subcomponents via a collection of axioms [11] This relationship is specified declaratively, abstracting away implementation concerns. Formally, an architecture ....

....and form the basis for correctness proof of the refinement mappings. This work would be an ideal mechanism to specify links between architecture theories and architecture implementations. Our chosen methodology is an extension of the work done on Kestrel s Interactive Development System (KIDS) [16, 17, 18, 19]. In KIDS, the structure of specific algorithms such as global search or divide and conquer are represented as algebraic theories. The construction of algorithms is directed by a hierarchical arrangement of the algorithm theories [17] as well as special design tactics [19] Currently, the program ....

[Article contains additional citation context not shown here]

Douglas R. Smith and Micheal R. Lowry. Algorithm Theories and Design Tactics. Science of Computer Programming, 14:305--321, 1990.

....to operate on a higher level of abstraction and must be based on comprehensible formalizations of application domains and programming concepts rather than on low level inferences of the logical calculus. Algorithm design strategies based on schematic solutions for certain classes of algorithms [40] have proved to be suited best for this purpose since they can be formulated almost entirely in programmer s terminology. It has been demonstrated [41] that algorithm schemata do not only lead to a very efficient synthesis process but can also produce competitive algorithms if properly guided. ....

....partial) computable function body:D6 Set(R) together form a program. A program is correct if it computes the complete set of output values for each acceptable input (8x:D. I(x) body(x) fz:R j O(x,z)g) A specification is satisfiable if it can be extended into a correct program. As in [40] we use a formal notation for programs which emphasizes that we are interested in computing the set of all solutions of a given problem (assuming that there are finitely many) FUNCTION f(x: D) Set(R) WHERE I(x) RETURNS fz j O(x; z)g j body(x) The name f can be used in the body in order to ....

D. R. Smith & M. R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14(2-3):305--321, 1990.

....approach, through which incrementalities can be discovered in existing programs written in standard languages. Smith s work in KIDS [39, 40] is closely related to ours. KIDS is a semi automatic program development system that aims to derive efficient programs from high level specifications [41], as is APTS. Its version of finite differencing was developed for the optimization of its derived functional programs and has two basic operations: abstraction and simplification. Abstraction of a function f adds an extra cache parameter to f . Simplification simplifies the definition of f given ....

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14:305--321, 1990.

.... mechanism underlying two methods of constructing larger theories from smaller ones: extension and parameterization [13] A theory morphism maps the sorts and operators of one theory to sorts and operators of another theory such that the axioms of first theory are theorems in the second theory [14]. Theory B is an extension of theory A if B contains all of the sorts, operators and axioms of A. An extension is represented by a theory morphism from A to B that maps each sort and operator to itself in the target theory. A parameterized theory is a pair of theories: a parameter theory and a ....

....If execution of C is begun in a state satisfying I C , then it is guaranteed to terminate in a finite amount of time in a state satisfying OC . 3] A component interface specification can be represented formally as a component theory. A component theory is an extension of a problem theory [14]. A problem theory specifies the relationship between the domain and range of a specification and the precondition and postcondition, as shown in Figure 3(a) To specify a specific problem, the general problem theory is extended by adding definitions for the domain, range, precondition and ....

Douglas R. Smith and Micheal R. Lowry. Algorithm Theories and Design Tactics. Science of Computer Programming, 14:305--321, 1990.

....Part of the research reported herein has been funded by the German Federal Ministry of Research and Technology (BMFT) under contract no. 01 IS 203 K5 (KORSO) specific problem, synthesize a solution to this problem. These algorithm theories have intensively been investigated by Doug Smith [12, 13, 14] who defines, among other things, a hierarchy of algorithm theories encoding well known programming paradigms such as divide and conquer, global search, generate and test and others. However, his approach is only semi formal, some important aspects remain informal. The transformations developed ....

....the formalized steps since the type check mechanism of PVS produces the required proof obligations automatically. There are of course some aspects which can be improved in future versions of PVS. For example, when representing hierarchies of software development steps following the ideas of Smith [14] it is desirable to define theories which have other theories as their parameters. This is not possible in the current version. Furthermore, it is not possible to express properties about theories such as refinements between theories (theory morphisms) PVS does not allow types as parameters or ....

Douglas R. Smith and Michael R. Lowry. Algorithm Theories and Design Tactics. Science of Computer Programming, (14):305--321, 1990.

....approach, through which incrementalities can be discovered in existing programs written in standard languages. Smith s work in KIDS [38, 39] is closely related to ours. KIDS is a semi automatic program development system that aims to derive efficient programs from high level specifications [40], as is APTS. Its version of finite differencing was developed for the optimization of its derived functional programs and has two basic operations: abstraction and simplification. Abstraction of a function f adds an extra cache parameter to f . Simplification simplifies the definition of f given ....

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14:305--321, 1990.

....sizes of the subsets. Their top down analysis reveals that the asymmetric part of Darlington s tree can in fact be made symmetric, as Barstow points out in [1] This is due to the fact that they derive bubble sort and sinking sort as in place versions of selection sort and insertion sort . Smith [15, 16] describes a method for synthesising divide and conquer algorithms by top down decomposition of specifications into subproblem specifications, followed by bottom up composition of (concrete) programs synthesised for the subproblems. The decomposition and composition is done according to a chosen ....

Smith, D.R.: The Design of Divide and Conquer Algorithms. Science of Computer Programming 5, 37-58(1985)

....systematic approach. Using this approach, incrementalities can be discovered in existing programs written in standard languages. KIDS[37, 38] is a semiautomatic program development system that aims to derive programs from high level specifications, as is APTS. The system performs algorithm design[39], deductive inference, program simplification, partial evaluation, finite differencing, data type refinement, etc. Its version of finite differencing was developed for the optimization of its derived functional programs and has two basic operations: abstraction and simplification. Abstraction of a ....

D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14:305--321, 1990.

....they adopt an informal (first order) predicate logic notation for programs. Green Barstow[8, 1] have used their system for automatic program synthesis to demonstrate the synthesis of programs for the same six sorting algorithms that Darlington derived, using the divide and conquer paradigm. Smith[18, 19] derives merge sort , insertion sort , quick sort , and selection sort using a method for synthesising divide and conquer algorithms by top down decomposition of specifications into subproblem specifications, followed by bottom up composition of (concrete) programs synthesised for the subproblems. ....

D.R. Smith, The Design of Divide and Conquer Algorithms, Science of Computer Programming 5, 37-58 (1985).

....includes definitions for the types of movement record, resource, trip (a record comprised of start time and manifest) and schedule (a map from resource to sequence of trip) 15 5.1. 2 Algorithm Theories An algorithm theory represents the essential structure of a certain class of algorithms A [43]. Algorithm theory A extends problem theory B with any additional sorts, operators, and axioms needed to support the correct construction of an A algorithm for B. A theory morphism from the algorithm theory into some problem domain theory provides the problemspecific concepts needed to construct ....

....steps will however reduce these tests to fast and irredundant form. For example, the first test will reduce to checking that when we place a movement record mvr on trip t, we check that the POE of mvr and t are consistent. For details of deriving pruning mechanisms for other problems see [34, 42, 43, 35]. 5.2.3 Cutting Constraints and Constraint Propagation Constraint propagation is a more general technique that is crucial for early detection of infeasibility. We developed a general mechanism for deriving constraint propagation code and applied it to scheduling. Each node in a backtrack tree ....

[Article contains additional citation context not shown here]

Smith, D. R., and Lowry, M. R. Algorithm theories and design tactics. Science of Computer Programming 14, 2-3 (October 1990), 305--321.

....of fewer faults made in development and early detection of faults. Qualitative experience is reported in [14] and a quantitative analysis of the results in [13] In particular it was found that animation, test case generation and proof are all cost effective ways to find faults in formal texts [12]. The Spectrum project (1997) was a feasibility study into the commercial viability of intergating the VDM Toolbox and B Toolkit. The evaluation was undertaken from three perspectives: the industrial benefit of using the combined tool, the technical feasibility of the combination of the two tools ....

....different phases of the lifecycle favoured by the two methods and the complementary features currently provided by each toolkit. 3. 2 MaFMeth : The Measurement and Analysis of a Formal Method The combination of VDM and B was first explored by RAL and Bull Information Systems in the MaFMeth Project[13, 12]. This project developed part of a transaction management system using VDM for the initial design and analysis, and then translating into B for development and code generation. The formal development was part of the second release of an application integration product of the type often known as ....

Making the most of formal specification through Animation, Testing and Proo f. J.C. Bicarregui, J. Dick, B. Matthews, E. Woods. Science of Computer Programming, Vol. 29. (1997), Elsevier Science.

....domain as a parameterized domain theory. 2. representation of programming knowledge we also use theories to capture knowledge of algorithms and data structures. The logical concept of interpretation between theories is the basis for applying programming knowledge in the form of theories [3, 12, 10]. 1 This research was supported in part by the Office of Naval Research under Grant N0001490 J 1733 and in part by Air Force Office of Scientific Research under Contract F49620 91C 0073. Most, if not all, sorting algorithms can be derived as interpretations of the divide and conquer ....

Smith, D. R., and Lowry, M. R. Algorithm theories and design tactics. Science of Computer Programming 14, 2-3 (October 1990), 305--321.

....the compilation by the programmer as an advice to the compiler. This approach has been called extended compilation ( 4] In our setting additional information can be naturally expressed by algebraic properties. Moreover, optimization tactics themselves can be expressed by algorithm theories [13], leading to a knowledge based extendable compilation system. We illustrate the principal ideas of this approach by an example. The following function computes the chromatic number of a graph G. def chromaticNumber(G) if complete (G) then cardinality(nodes(G) else ....

Douglas R. Smith and Michael R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14:305--321, 1990.

.... to apply it to concrete problem specifications may be found in [7, 14] The general idea underlying the algorithm design tactics in KIDS is to represent abstract knowledge about a class of algorithms (such as divide and conquer or dynamic programming) as a theory, called an algorithm theory [9]. Models of an algorithm theory correspond to instances for a particular problem (e.g. quicksort and mergesort are two distinct models of divide andconquer theory) Constructing an algorithm for a formally specified problem corresponds to constructing an interpretation from an algorithm theory to ....

Smith, D. R., and Lowry, M. R. Algorithm theories and design tactics. Science of Computer Programming 14, 2-3 (October 1990), 305--321.

....optimization steps in KIDS will however reduce these tests to their nonredundant essense. For example, the first test will reduce to checking that when we place a movement record mvr on trip t, the POE of mvr and t are consistent. For details of deriving pruning mechanisms for other problems see [16, 19, 17, 18]. Figure 1: Global Search Subspace and Cutting Constraints 4.2.2 Cutting Constraints and Constraint Propagation Constraint propagation is another mechanism that is crucial for early detection of infeasibility. We developed a general mechanism for deriving constraint propagation code and applied ....

Smith, D. R., and Lowry, M. R. Algorithm theories and design tactics. Science of Computer Programming 14, 2-3 (October 1990), 305--321.

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.