A Formalization of Programs in First-Order Logic with a Discrete Linear Order

We consider the problem of representing and reasoning about computer programs, and proposea translator from a core procedural iterative programming language to first-order logic with quantification over the domain of natural numbers that includes the usual successor function and the ``less than'' linear order, essentially a first-order logic with a discrete linear order. Unlike Hoare's logic, our approach does not rely on loop invariants. Unlike typical temporal logicspecification of a program, our translation does not require a transition system model of the program, and is compositional on the structures of the program. Some non-trivial examples are given to show the effectiveness of our translation for proving properties of programs.