TL;DR
Matrix Code introduces a mathematical semantics to imperative programming, enabling incremental development from specifications and ensuring correctness through fixpoints, with an abstract dual-state machine model.
Contribution
It provides a novel formal framework for imperative programming with mathematical semantics and a new abstract machine model, enhancing correctness and development process.
Findings
Matrix Code offers a formal semantics for imperative programs.
Programs are developed incrementally from pre/post-conditions.
Correctness is characterized by fixpoints of a transformation.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsRobotic Mechanisms and Dynamics · Scheduling and Optimization Algorithms