A Weakest Precondition Model for Assembly Language Programs, unpublished manuscript

I am indebted to Prof. Edsgar Dijkstra for introducing me to weakest preconditions, Prof. J Moore for identifying early work of John McCarthy in transforming imperative programs to their functional counterparts, and to Dr. Frank Rimlinger for many fruitful discussions on the implementation of the ideas in this paper. 2.0 Overview This paper describes a formal model, based upon Dijkstra’s weakest preconditions [4], for reasoning about assembly language programs. The model applies more generally to any finite state machine. It extends earlier work of Floyd [5], Hoare [10] and Dijkstra [4], by automatically generating closed form expressions for the weakest precondition of arbitrary loops. Section 3 provides an informal introduction to the subject matter, followed by a more rigorous treatment in sections 4 and 5. Finally, section 6 briefly compares this to other work. 3.0 Preliminaries 3.1 Functional Programs Reasoning about computer programs requires that program variables have well defined meaning. An imperative program may associate different values with a variable X depending on the state of its execution. This is not true of purely functional programs, which model computation using a composition of state-to-state transformations. By way of illustration, consider a program which sums the first N natural numbers