State-Transition Computation Models and Program Correctness Thereon
Kiyoshi Akama, Ekawit Nantajeewarawat · Journal of Advanced Computational Intelligence and Intelligent Informatics · 2007
The common framework for formalizing state-transition computation models we present is based on a general theory for studying the interrelationship of specifications, programs, computation, and program correctness. We establish a necessary and sufficient condition for program correctness for this class of computation models and demonstrate framework application by formalizing, as its instances, two concrete examples of state-transition computation models – NAT and D-rule. We compare their correct-program spaces by introducing the embedding mapping concept.