A Weakest Precondition Model for Assembly Language Programs
Wilfred J. Legato · 2003
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.