Nodeterminism and communication in functional programming systems : A study in formal program development

Abstract

The phenomenal advancement in VLSI technology witnessed in recent years has led to the economic feasibility of building computers which support massive parallelism in computation. Functional programming languages have great potential for becoming the programming languages for these future generation computers because functional programs compute by value and retain the parallelism in the algorithms they describe. Functional languages also possess the most elegant mathematical properties required in the formalisms for programming. Functional Programming (FP) Systems of Backus are among those functional languages which offer powerful tools for programming and are compatible with the highly parallel architectures for future generation computers. However, several important programming concepts such as nondeterminism in programs and inter-program communication have not been adequately investigated in the context of FP systems. In this dissertation, we present, with program development as our principal objective, our work on choice nondeterminism and inter-program communication in certain extended and modified versions of FP systems, called Nondeterministic FP (NFP) systems, which are introduced in this dissertation. Several new functionals (or program-forming operations) are used in NFP systems; one of these introduces nondeterminism into programs while the others contribute significantly to the simplification and enrichment of the algebraic methods of reasoning about programs. The requisite mathematical semantics of NFP programs is presented. Several techniques of program transformation for reasoning about and development of programs are proposed. In order to ensure correctness of the initial specification of a program (to be developed), two complementary approaches to formal program specification are introduced. Algebraic methods for development of programs from their specifications are also described. Finally, some preliminary results of our investigative work on the introduction of inter-program communication into NFP systems, and on the algebraic methods of reasoning about and development of communicating programs are presented. Illustrative examples are used to explain the various programming concepts. Most of the programming concepts proposed for NFP systems can be easily adopted to FP systems, thereby strengthening the programming aspects of the latter systems.