Computer programs are language expressions of computations in terms of both the computer, as their computing agent, and behavior, as the computation they represent. Reasoning about computer programs is difficult because of the different natures of the computers and of the computations they perform. Various programming languages use various logics to express program properties. Reactive and concurrent computations use temporal logics where computations are seen as state transitions.

Procedural languages may use various first-order logics, such as the Hoare logic, which expresses computations’ properties by predicates that remain invariant by the computations performed by program statements. The paper we discuss here uses another approach. Computations expressed by program statements are captured as variable values before and after the computation expressed by those statements, which in fact is the same as is done with temporal logic. However, the author relies on a first-order logic with a discrete linear order to express a program computation as a first-order theory with quantification over natural numbers.

The long-term goal of the research presented in this paper is the development of a translator to map a programming language into the first-order logic. Hence, the author envisions the automatic generation of the axioms defining the first-order theory representing the program computation. The body of the work consists of showing the first-order theories representing the computations encapsulated in various kinds of program statements. The mechanism of mapping a program into a first-order theory is illustrated on some classic algorithms, such as Cohen’s integer division algorithm. When properties of programs during their execution are discussed, the author uses labeled programs, which are very similar to labeled transition systems used by Manna and Pnueli in their book [1]. But there is no reference to this book. It would be interesting to see the relationship between the algebraic theory representing the computation expressed by a program, as discussed in this paper, and the language used by Manna and Pnueli to represent the computations expressed by various transition systems. Since this language was used to express the computation performed by a software system [2], such a relationship would represent a real step toward the translator envisioned by the author.