Matrix Code
Programming Languages
2013-02-26 v6
Abstract
Matrix Code gives imperative programming a mathematical semantics and heuristic power comparable in quality to functional and logic programming. A program in Matrix Code is developed incrementally from a specification in pre/post-condition form. The computations of a code matrix are characterized by powers of the matrix when it is interpreted as a transformation in a space of vectors of logical conditions. Correctness of a code matrix is expressed in terms of a fixpoint of the transformation. The abstract machine for Matrix Code is the dual-state machine, which we present as a variant of the classical finite-state machine.
Cite
@article{arxiv.1109.5416,
title = {Matrix Code},
author = {M. H. van Emden},
journal= {arXiv preprint arXiv:1109.5416},
year = {2013}
}
Comments
39 pages, 19 figures; extensions and minor corrections