Some results concerning proofs of statements about programs

Abstract

A programming language is viewed as a language for expressing "instructions" for a computation to be performed by a particular machine. A class of abstract machines (which includes universal machines) is defined. These machines are viewed as devices which execute "instructions" expressed in programming languages. Using this model and an appropriate definition of a programming language, it is shown that there is at least one system of logic which has the following properties for all machines in this class.o(1) For three concepts of the equivalence of computations and of programs, this system can be used to show that two computations or programs are or are not equivalent.(2) Given a program and a finite number of functions, this system can be used to show that the program does or does not specify the computation of these functions. That is, it is shown that certain relations of equivalence among programs and the relation of a program to the functions whose computation it specifies probably obey the law of excluded middle in this system of logic. © 1970 Academic Press, Inc.