PROGRAM CONTROL AS A SET‐THEORETIC CONCEPT
J. R. Jefferson Wadkins · ETS Research Report Series · 1994
A point does not move, a circle does not shrink, a number does not change its value, and a function does not decrease.Each of these mathematical entities is a set; it is static; it takes no action; it does not change; it just sits there being a set.Nevertheless, the notion of variable mathematical entities is present in most mathematical activities and permeates the teaching of mathematics.Thus teachers feel no shame in saying things like "as the point (r,A) moves from right to left on this curve, the circle with radius r shrinks...", because they are justifiably confident that the language they use, which employs the notion of variable mathematical entities, can be converted to the static language of set theory in the context of axioms for a complete ordered field.While there are purists who frown upon use of "variables" in serious mathematical discourse, most mathematicians are comfortable with such phraseology because of the existence of precise semantics that legitimize these notions in terms of set-theoretic concepts from which the purist might prefer never to emerge. PURPOSE AND MOTIVATION FOR THIS PAPERPrecise proofs of program correctness and precise proofs in calculus are arguments about static entities.Both are typically introduced with teacher as actor and students as spectators, but there is an implicit understanding that students are only being "exposed" to these techniques.The answer to the ever-present, student-as-spectator question, "Are we responsible for this on the next test?" is almost always negative in both cases.However, there is a vast difference in how introductory courses handle intuitive notions consistent with corresponding precise ideas.In typical beginning calculus courses, the notion of "variable" is employed to give plausibility arguments for fundamental theorems that are seldom stated in such courses very precisely, and seldom justified with epsilon-delta arguments; but students do gain an appreciation of the fundamental nature of such theorems by constantly taking part in both home-work exercises and classroom activities that employ "variables" to reason about specific applications of those fundamental theorems.Although there is a programming notion used in introductory courses for other purposes that could be used to give convincing arguments for both fundamental theorems of program correctness and instances of their application to code written by beginning programmers, use of this intuitive notion in teacher presentations which give plausibility arguments that code segments satisfy their informal specifications would seem to be relatively rare.That programming notion is "program control", an entity used by both neophytes and professional programmers for "desk checking" of code before testing it.The readiness of mathematics teachers to use hand-waving arguments in calculus presentations, as opposed to the hesitancy of computer science teachers to use the notion of "program control" in their classroom presentations, is probably best explained by the fact that "real variables" have a widely understood logical basis, while "program control" is often thought to be a mere heuristic, unrelated (indeed, contrary to) precise proofs of correctness about static entities employing the weakest-precondition predicate transformer.Use of "program control" provides a short and simple argument for a fundamental theorem of program correctness', which Edsger Dijkstra stated without proof in his seminal 1975 paper [1] and whose proof, using the symbolism and tools of the formal predicate calculus, is outlined (as the answer to three exercises) taking up more than two pages of densely packed symbolism in The Science of Programming by David Gries [2].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 our version of that fundamental theorem.We would venture to claim that both the statement and proof of our version of this theorem (as given in the next section) can be made understandable by, and convincing to, typical beginning students who have no preparation other than what is typically offered in the first half of CS1 --and that this can be accomplished with very little effort on the part of the teacher.This is clearly not the case with even the statement of the theorem in the development of either Dijkstra [1] or Gries [2].• That argument and that theorem is given at the beginning of Section 1.1.