skip to main content skip to footer

Program Control as a Set-Theoretic Concept

Author(s):
Wadkins, J. R. Jefferson
Publication Year:
1994
Report Number:
RR-94-56
Source:
ETS Research Report
Document Type:
Report
Page Count:
27
Subject/Key Words:
Computer Science, Programing, Set Theory

Abstract

Use of "program control" provides a short and simple argument for a fundamental theorem of program correctness. The purpose of this paper is to provide operational semantics for imperative programming languages that legitimize the phraseology used in the statement and proof of one version of that fundamental theorem. The goal of the paper was to legitimize the use of the appealing operational language used in the statement and proof of theorem 1.1.1 by defining "program control" and other operational concepts in terms of set theory. There were two key elements in the development of these definitions. One was a distinction that is not often made, and the other was a unifying use of a definition not often insisted upon. The distinction was between sequences and strings, with strings defined as equivalence classes of sequences. The unifying use was of the definition of a sequence as a function, a function as a relation, and a relation as a set. Once the definition of an imperative programming language system was developed, all of the familiar terms used in discussing programs and programming could be defined as sets. In particular, all of the language used in Theorem 1.1.1 and its proof could be defined in set-theoretic terms. The two most prominent such terms were "program control" and "execution of a program segment." Finally, each of the questionable words and phrases used in the statement and proof of fundamental Theorem 1.1.1 was translated into the precise set- theoretic terms defined in Section 2. (JGL) (27pp.)

Read More