Testing and verification aspects of Pascal-like languages

This paper addresses aspects of programming language design that affect the ease with which programs written in a language can be subjected to systematic testing and/or program verification. The discussion focuses of Pascal and on several languages that have been derived primarily from Pascal, particularly Euclid and PLAIN. Specific language issues addressed include translation-time checking, program readability, flow of control, support for program modularity, data flow, and program immutability. The relative ease of validating such programs is then determined by the style in which the programs are written. The paper presents some guidelines for writing programs in Pascal-like languages for testability and verifiability.