perm filename FOURTN.MSS[BIB,CSR]2 blob sn#617098 filedate 1981-10-16 generic text, type C, neo UTF8

COMMENT ā VALID 00002 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 @Entry(Code "STAN-CS-81-870", C00008 ENDMK Cā; @Entry(Code "STAN-CS-81-870", Title "Optimal Pagination Techniques for Automatic Typesetting Systems", Author "Michael F. Plass", Price "$4.30", not available, Note "77 pages", Date "June 1981") @Entry(Code "STAN-CS-81-871", Title "Good Layouts for Patern Recognizers", Author "Howard W. Trickey", Price "$2.45", not available, Note "15 pages", Date "August 1981") @Entry(Code "STAN-CS-81-872", Title "Synthesis of Communicating Processes from Temporal Logic Specifications", Author "Zohar Manna and Pierre Wolper", Price "$2.85", FREE, Note "28 pages", Date "September 1981") In this paper, we apply Propositional Temporal Logic (PTL) to the specification and synthesis of the synchronization part of communicating processes. To specify a process, we give a PTL formula that describes its sequence of communications. The synthesis is done by constructing a model of the given specifications using a tableau-like satisfiability algorithm for PTL. This model can then be interpreted as a program. @Entry(Code "STAN-CS-81-873", Title "Virtual Memory Management", Author "Richard William Carr", Price "$8.90", FREE, Note "230 pages", Date "August 1981") @Entry(Code "STAN-CS-81-874", Title "Multiprocessing Architectures for Local Computer Networks", Author "Alfred Z. Spector", Price "$5.75", FREE, Note "125 pages", Date "August 1981") @Entry(Code "STAN-CS-81-875", Title "Computation of Matrix Chain Products, Part I, Part II", Author "T. C. Hu and M. T. Shing", Price "$5.70", FREE, Note "124 pages", Date "September 1981") This paper considers the computation of matrix chain products of the form (M[1] x M[2] x...x M[n-1]). If the matrices are of different dimensions, the order in which the matrices are multiplied affects the number of operations. An optimum order is an order that minimizes the total number of operations. We present some theorems about an optimum order of multiplying the matrices. Based on these theorems, an O(n log n) algorithm for finding an optimum order is presented. @Entry(Code "STAN-CS-81-877", Title "Verification of Sequential Programs: Temporal Axiomatization", Author "Zohar Manna", Price "$3.35", FREE, Note "45 pages", Date "September 1981") This is one in a series of reports describing the application of temporal logic to the specification and verification of computer programs. In earlier reports, we introduced temporal logic as a tool for reasoning about concurrent programs and specifying their properties and presented proof principles for establishing these properties. Here, we restrict ourselves to deterministic, sequential programs. We present a proof system in which properties of such programs, expressed as temporal formulas, can be proved formally. Our proof system consists of three parts: a general part elaborating the properties of temporal logic, a domain part giving an axiomatic description of the data domain, and a program part giving an axiomatic description of the program under consideration. We illustrate the use of the proof system by giving two alternative formal proofs of the total correctness of a simple program.