Imperative programming verification is a serious problem! Parallel development of proof and code for imperative programming is the proposed solution. A new language is presented to create a proof in parallel with the code called matrix code, which is based on an extension of finite state machines (FSMs) called dual state machines (DSMs). Programs are represented as a matrix and the elements are binary relations among data states. The construct of the matrix is explained with clarity and a logical progression of building the theoretical foundations and then providing small, conceptually contained examples.

The problem is characterized as addressing only “hard-core” imperative code, or that which would not have extensions to support functional programming. This restriction creates an academic construct of orthogonality that does not typically exist. Many general programming languages are flexible enough to support imperative and functional paradigms. For instance, C# 3.0 and Visual Basic 9.0 have extensions to support functional programming that include type inference and lambda expressions. Although this is an artificial construct, it serves a solid instructional purpose of reducing the complexity of the concepts and providing a focused view of imperative program verification. The author provides the necessary definitions, theorems, lemmas, and proofs for the semantics of DSMs, or directs the reader to references of prior work.

This 21-page paper is well written with many examples of using matrix code in the application of DSMs. The relevancy of the topic to current best practices might be better explored; the author provides 19 references and all but two predate the year 2000. The matrix code language to support parallel development of proof and code is straightforward in the examples provided, but might prove daunting if applied to a large development project.