Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
433929 | Science of Computer Programming | 2014 | 19 Pages |
•New programming language for imperative programming.•Allows parallel development of code and correctness proof.•Is based on enhanced finite-state machine.
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.