Top-down synthesis of simple divide and conquer algorithms
Abstract
A new method is presented for the deductive synthesis of computer programs. The method takes as given a formal specification of a user's problem. The specification is allowed to be incomplete in that some or all of the input conditions may be omitted. A completed specification plus a computer program are produced by the method. Synthesis involves the top-down decomposition of the user's problem into a hierarchy of subproblems. Solving each of these subproblems results in the synthesis of a hierarchically structured program. The program is guaranteed to satisfy the completed specification and to terminate on all legal inputs. In this paper we present a framework for a top-down synthesis process, explore the structure of a class of divide and conquer algorithms, and present a method for the top-down synthesis of algorithms in this class. Detailed derivations of four sorting algorithms are presented. (Author)
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.NPS Report Number
NPS-52-82-011Related items
Showing items related by title, author, creator and subject.
-
A heuristic for decomposing a problem into a sequence of subproblems.
Evans, Donald Vincent (Monterey, California. Naval Postgraduate School, 1982-12);This thesis presents a method for decomposing a specification of a problem into a sequence of subproblem specifications. The method uses the specification to build a tree-like structure called a semantic net. The net is ... -
Large-domain discrete integration techniques for the wave equation as an aid in the calculation of propagation loss and the study of adaptive acoustic arrays
Johnson, Roy Martin (Monterey, California. U.S. Naval Postgraduate School, 1969-10);This work is concerned with two inter-related problems: (1) the theory and application of algorithms for the discrete integration of the acoustic wave equation in large, multi-dimensional, variable-parameter domains and, ... -
Structural computer-aided design of current-mode CMOS logic circuits
Onneweer, Step; Kerkhoff, Hans; Butler, Jon T. (1988-05);A set of CAD tools for the synthesis and layout generation of multiple-valued current-mode CMOS logic (CMCL) circuits is described. The synthesis method is based upon the cost-table method. The general circuit ...