کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
433929 | 1441690 | 2014 | 19 صفحه PDF | دانلود رایگان |
• 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.
Journal: Science of Computer Programming - Volume 84, 1 May 2014, Pages 3-21