The programming language Alphard is designed to provide support for both the methodologies of "well-structured" programming and the techniques of formal program verification. Language constructs allow a programmer to isolate an abstraction, specifying its behavior publicly while localizing knowledge about its implementation. The verification of such an abstraction consists of showing that its implementation behaves in accordance with its public specifications; the abstraction can then be used with confidence in constructing other programs, and the verification of that use employs only the public specifications.

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.

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.