Language Features that Support Program Verification (illustrated in PL/C)

Abstract

The author of a program can convince its readers (including himself) that it computes as he intended by writing into the program text a precise description of what it should do. This description can include a clear proof that the program behaves as advertised. In the future, programming languages may offer far more mechanical assistance in expressing, checking, and processing these descriptions than they do now. However, some existing languages, such as PL/C, provide features which help in these tasks considerably. Here we examine such features applied to simple programs of the type traditionally taught in beginning programming classes. We discuss various proposals for expanding programming languages to provide more assistance of this type. Keywords and phrases: program correctness, automatic program verification, Hoare axioms, Scott induction, recursive programs, least number operator, bounded quantifiers, inductive assertion method, programming language design, very high level programmng languages, PL/I, PL/C, macro facilities.