This paper provides operational semantics for imperative programming languages that legitimize the phraseology used in the statement and proof of a fundamental theorem of program correctness. Some of the phrases used in the theorem are normally undefined, but intuitively appealing. This paper attempts to give precise meaning to the questionable phrases in the theorem. The real value of this theorem lies in a corollary that provides a programming template for the construction of a loop with a built-in proof of its correctness just by writing two segments of straight-line code to fit given specifications (without having to visualize a repetitive process). In defining this language, a distinction is made between strings and sequences, with strings defined as equivalent classes of sequences. Also essential is the definition of an imperative programming language and of program control, which turns out to be a function mapping each pair consisting of a position (in the program) and a state into a (possibly different) pair also consisting of a position and a state. Appendixes present a minimal example and a proof of the theorem. (SLD)