Concurrency in Gypsy is based on a unique, formal approach to specifying and proving systems of concurrent processes. The specification and proof methods are designed so that proofs of individual processes are totally independent, even when operating concurrently. These methods can be applied both to terminating and non-terminating processes, and the proof methods are well suited to automated verification aids. The basic principles of these methods and their interaction with the design of Gypsy are described.

This paper is an initial progress report on the development of an interactive system for verifying that computer programs meet given formal specifications. The system is based on the conventional inductive assertion method: given a program and its specifications, the object is to generate the verification conditions, simplify them, and prove what remains. The important feature of the system is that the human user has the opportunity and obligation to help actively in the simplifying and proving. A general description is given of the overall design philosophy, structure, and functional components of the system, and a simple sorting program is used to illustrate both the behavior of major system components and the type of user interaction the system provides.

Since the publication of the Curriculum 68 report of the ACM Committee [CUR 68], undergraduate computer science programs have undergone substantial changes. Notably, many courses previously taught at the graduate level have shifted down to the undergraduate level; new areas have developed and consolidated but were not covered by the ACM report. These facts make it necessary to revise and update the Curriculum 68 report. An important factor which could help the revision is the actual experience gained through the development of many new undergraduate computer science programs since the publication of Curriculum 68 report five years ago. More specifically, most recommendations of the ACM report contain just the subject areas to be taught. The actual teaching experiences of these courses have formulated certain basic philosophies and formats of presentation. It is helpful, in our opinion, to compare the merits of these philosophies and formats of presentation.

A definition is given of computer interval arithmetic suitable for implementation on a digital computer. Some computational properties and simplifications are derived. An ALGOL code segment is proved to be a correct implementation of the definition on a specified machine environment.