Towards Increased Productivity of Algorithm Implementation


Table of Contents:

  1. Principal Investigator.
  2. Productivity Measures.
  3. Summary of Objectives and Approach.
  4. Detailed Summary of Technical Progress.
  5. Transitions and DOD Interactions.
  6. Software and Hardware Prototypes.
  7. List of Publications.
  8. Invited and Contributed Presentations.
  9. Honors, Prizes or Awards Received.
  10. Project Personnel Promotions.
  11. Project Staff.
  12. Multimedia URL.
  13. Keywords.
  14. Business Office.
  15. Expenditures.
  16. Students.
  17. Book Plans.
  18. Sabbatical Plans.
  19. Related Research.
  20. History.


Principal Investigator.


Productivity Measures.


Summary of Objectives and Approach.

  1. Our long term objective is to dramatically improve the programming productivity of algorithm implementation and labor-intensive software. Our approach is based on very high level compiler technology with a generic (as opposed to domain specific) problem domain, an automatic (as opposed to interactive) software development methodology, and the production of high performance (as opposed to prototype) code.
  2. During the grant reporting period, the emphasis has been on developing and applying formal semantics-based reasoning to simultaneously design algorithms, analyze their asymptotic complexity, and implement them in high performance code. One aspect of this approach involved the development of a type and subtype system that abstracts a sequential RAM model of computation, and that provides a high level set theoretic programming language with computational transparency. Another aspect involved the use of mechanical proof checking to prove the correctness of transformations that form the basic lemmas in a program derivation.


Detailed Summary of Technical Progress.

  1. Our initial thrust was to provide new semantic foundations for finite differencing based on Hoare Logic. Bard Bloom and I rewrote our paper for Science of Programming to incorporate these ideas, which allowed us to rederive more formally our new ready simulation algorithm and its asymptotic complexity analysis. The new derivation is ideally suited for mechanical proof checking, and Alfredo Ferro's group at the U. of Catania in Italy has taken up the challenge. Ferro and his colleage D. Cantone will be visiting Courant later this year to combine his expertise (in fast decision procedures in fragments of set theory) with our transformational methodology.
  2. Building on the more solid semantic ground of Bloom and Paige, Keller and I launched a difficult and comprehensive experiment to combine algorithm design, analysis, and implementation within a mechanically checked formal derivation. The type and subtype system developed earlier with Cai and Henglein was extended to support a computationally transparent partition datatype. This extension proved useful in deriving two new DFA minimization algorithms that improved upon the classical algorithms of Hopcroft and Cardon and Crochemore. The main proof obligation in the derivation was supported by 7000 lines of proofware that was passed through Keller's working set theoretic proof checker. Although the protracted labor involved in building and executing this proofware was almost overwhelming, the expense was somewhat offset by a successful reuse of major portions of these proofs. In particular, the DFA minimization algorithm is obtained by specializing and then extending the last step in the derivation of the a high level bisimulation algorithm. This work will appear in Comm. of Pure and Applied Math.
  3. Two other new results can be reported. With Klarlund and his team at the U. of Aarhus, a new improved incremental BDD-based DFA minimization algorithm was designed and implemented within the MONA verification tool. This tool makes use of the second order monadic calculus of strings, a succinct predicate oriented characterization of regular languages, in variaous applications of automatic verification. The work was reported at the TACAS software tool workshop, and our paper was selected for a special issue of LNCS.
  4. We have been studying Willard's RCS theory over a period of years in hopes of gaining incite into how language abstraction can be used to obtain algorithmic results. Under the assumption that hashing unit space data takes unit time, Willard defined subclasses of relational calculus queries that could be executed in low expected polynomial time and space with respect to the input/output space. Previously we reported that by associating expected complexity with set theoretic terms, Willard's proofs could be compressed by eliminating redundancy and by replacing raw counting arguments with more algebraic reasoning. We were also able to map the linear time fragment of RCS queries into the `simple' subclass of the linear time set theoretic language of Cai and Paige (cf. POPL 87). Last year with Deepak Goyal we used our computationally transparent type and subtype system to obtain an algorithmic improvement. By typing our set theoretic implementation of RCS, we were able to prove that the the linear time fragment of Willard's RCS queries can be implemented in linear worst case time.


Transitions and DOD Interactions.


Software and Hardware Prototypes.

  1. Prototype Name: Maximimum Ready Simulation Program


List of Publications.

  1. Bloom, B. and Paige, R., "Transformational Design and Implementation Of a New Efficient Solution to the Ready Simulation Problem," Science of Computer Programming, 24(3), June 1995, pp. 189-220.
  2. Bouma, W., Cai, J., Fudos, I., Hoffmann, C., and Paige, R., "A Geometric Constraint Solver," CAD, Vol. 27, No. 6, June, 1995, pp. 487-501.
  3. Cai, J. and Paige, R., "Using Multiset Discrimination To Solve Language Processing Problems Without Hashing," Theoretical Computer Science, vol 145, Num 1-2, July, 1995, pp. 189-228.
  4. Chang, C. and Paige, R., "From Regular Expressions to DFA's Using Compressed NFA's," accepted for publication, Theoretical Computer Science, 1995.
  5. Keller, J. P. and Paige, R., "Program Derivation With Verified Transformations - A Case Study," in The Houses That Jack Built, pp. 151 - 208, New York University, Proc. Symp. Celebrating the Scientific Trajectory of Jack Schwartz, ed. E. Schonberg, May, 1995, long form accepted in Communications of Pure and Applied Mathematics, Vol 48, 1995.
  6. Henriksen, J., Jensen, J., Jorgensen, M., Klarlund, N., Paige, R., Rauhe, T., and Sandholm, A., "Mona: Monadic Second-Order Logic In Practice," Proc. TACAS (Workshop on Tools and Algorithms for Construction and Analysis of Systems), BRICS Notes Series NS-95-2, U. of Aarhus, May, 1995, pp. 58-73,; selected to appear in LNCS, 1090, 1995.
  7. Paige, R., "Analysis and Transformation of Set-Theoretic Languages," Mini-Course Notes, BRICS Notes Series, NS-95-5, University of Aarhus, Aarhus, Denmark, August 1995.


Invited and Contributed Presentations.

  1. Seminar, U. of Lund, "Towards Increased Productivity of Algorithm Implementation," Aug. 1995.
  2. Seminar, U. of Lund, "Viewing A Transformational System at Work," Aug. 1995.
  3. Minicourse, 4 Lectures with System Demonstration at the BRICS Center, U. of Aarhus, "Analysis and Transformation of Set-Theoretic Languages", Aarhus, Denmark, Aug. 1995.
  4. Presentation at Atlantique Workshop, "A Reconstruction and Extension of Willard's Predicate Retrieval Theory," San Diego, CA., June 1995.
  5. Presentation at Symp. Celebrating the Scientific Trajectory of Jack Schwartz, "Program Derivation With Verified Program Transformation - A Case Study," New York City, May 1995.
  6. MASPLAS 95, Research in Transformational Programming at NYU, D. Goyal, A. Leung, M. Marinescu, R. Paige, A. Rudra, C. Yung E. Stroudsburg, PA., Apr. 1995.


Honors, Prizes or Awards Received.

  1. Invited Speaker at Symp. Celebrating the Scientific Trajectory of Jack Schwartz, New York City, May 1995.


Project Personnel Promotions.


Project Staff.

  1. Name: Dr. Robert Paige


Multimedia URL.

  1. EOYL FY95
  2. QUAD FY95
  3. EOYL FY94
  4. Research Project
  5. U. of Aarhus On-Line Minicourse on Research
  6. Citation To Project Found at CMU in home page on Semantics-Based Program Analysis and Manipulation


Keywords.

  1. Transformations
  2. Algorithm Derivation
  3. Program Development
  4. Productivity


Business Office


Expenditures

  1. Est. FY96: 100%
  2. FY95: 90%
  3. FY94: 98%


Students

  1. Name: [Mr|Ms|Dr] Student_name_goes_here


Book Plans


Sabbatical Plans


Related Research

  1. Semantics-Based Program Analysis and Manipulation
  2. IFIP Working Group 2.1---Algorithmic Languages and Calculi
  3. BRICS (Basic Research in Computer Science, U. of Aarhus


History