Accession Number : ADA193996

Title :   The Origin of a Binary-Search Paradigm. Revision.

Descriptive Note : Technical note,

Corporate Author : SRI INTERNATIONAL MENLO PARK CA

Personal Author(s) : Manna, Zohar ; Waldinger, Richard

PDF Url : ADA193996

Report Date : Oct 1986

Pagination or Media Count : 51

Abstract : In a binary-search algorithm for the computation of a numerical function, the interval in which the desired output is sought is divided in half at each iteration. This paper considers how such algorithms might be derived from their specifications by an automatic system for program synthesis. The derivation of the binary-search concept has been found to be surprisingly straightforward. The programs obtained, though reasonably simple and efficient, are quite different from those that would have been constructed by informal means. Keywords: Program synthesis; Theorem proving; Binary search, Real square root, Lambo function; Deductive tableau system; Computer programming.

Descriptors :   *ALGORITHMS, AUTOMATIC, COMPUTER PROGRAMMING, NUMERICAL ANALYSIS, SEARCHING, SQUARE ROOTS, COMPUTATIONS, ITERATIONS, FUNCTIONS(MATHEMATICS)

Subject Categories : Numerical Mathematics

Distribution Statement : APPROVED FOR PUBLIC RELEASE