Program Composition Notation

Abstract

Program Composition Notation (PCN) is a notation for composing programs. The programs that are composed may be expressed in base languages, such as Fortran, Lisp, or Strand or in PCN itself. The PCN research effort has a narrow focus. The chapter explains the program composition operators. The traditional method of constructing programs is by sequential composition. The chapter presents the evaluation the thesis that other forms of program composition are helpful, and that programmers should be able to define their own composition operators for program composition. A goal of an effort is to identify proof rules for the composition operators, and to evaluate their efficacy in reasoning about programs. A unifying framework has been proposed for developing numeric, symbolic, and reactive programs. The focus is to develop programs by stepwise refinement, starting with programs with simpler proofs and refining them if they are not adequately efficient. PCN is an outgrowth of UNITY and Strand. It has the basic data types: boolean, integer, single and double precision floating point number, character, and string. The initial value of a variable of a basic data type is arbitrary. The chapter also explores that a PCN has a data type called synch, for synchronization. The initial value of a synch variable is a special symbol, φ that indicates that the variable is undefined. Programmers have the obligation of proving that a synch variable is assigned at most one value. Given such a proof, a synch variable is both undefined (φ), or it is defined and its definition remains unchanged. A synch variable can be assigned a value of any type.