Matrix Code: A Language for Parallel Development of Code and Proof

A program in matrix code is a matrix that can be interpreted in three ways. First, it is an executable program. Second, the matrix can be interpreted as a set of Floyd verification conditions that prove the program partially correct. Third, the matrix can be interpreted as a transformation in a generalized vector space. The authors relate the algebra of such transformations to the program's specification and behaviour. The advantage of matrix code is that it supports verification-driven programming, a method for the parallel development of correctness proof and code. They present examples of such development including one that illustrates gain in efficiency not easily obtainable with conventional control structures.