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.

Provided by: University of Victoria Topic: Software Date Added: Nov 2011 Format: PDF

Find By Topic