State-Transition Computation Models and Program Correctness Thereon
Kiyoshi Akama* and Ekawit Nantajeewarawat**
*Division of Large-Scale Computational Systems, Information Initiative Center, Hokkaido University, Kita 11 Nishi 5, Kita-ku, Sapporo, Hokkaido 060-0811, Japan
**Computer Science Program, Sirindhorn International Institute of Technology, Thammasat University, Rangsit Campus, P.O. Box 22, Thammasat-Rangsit Post Office, Pathumthani 12121, Thailand
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.
-  K. Akama and E. Nantajeewarawat, “Formalization of Computation Models in View of Program Synthesis,” in Proc. the 4th Int. Conf. on Intelligent Technologies, Chiang Mai, Thailand, pp. 507-516, 2003.
-  J. W. Lloyd, “Foundations of Logic Programming,” second, extended edition, Springer-Verlag, 1987.
-  T. Frühwirth, “Theory and Practice of Constraint Handling Rules,” Journal of Logic Programming, Vol.37, pp. 95-138, 1998.
-  J. Jaffar, M. Maher, K. Marriott, and P. Stuckey, “The Semantics of Constraint Logic Programs,” Journal of Logic Programming, Vol.37, pp. 1-46, 1998.
-  R. Bird, “Introduction to Functional Programming,” second edition, Prentice Hall, 1998.
-  K. Akama, Y. Shigeta, and E. Miyamoto, “Solving Logical Problems by Equivalent Transformation – A Theoretical Foundation,” Journal of the Japanese Society for Artificial Intelligence, Vol.13, pp. 928-935, 1998.
-  K. Akama and E. Nantajeewarawat, “Formalization of the Equivalent Transformation Computation Model,” Journal of Advanced Computational Intelligence and Intelligent Informatics, Vol.10, No.3, pp. 245-259, 2006.
-  Y. Gurevich, “Sequential Abstract-State Machines Capture Sequential Algorithms,” ACM Transactions on Computational Logic, Vol.1, No.1, pp. 77-111, 2000.
-  E. Börger and R. Stärk, “Abstract State Machines: A Method for High-level System Design and Analysis,” Springer-Verlag, 2003.
-  C. A. Petri, “Nets, Times and Spaces,” Theoretical Computer Science, Vol.153, pp. 3-48, 1996.
-  N. Dershowitz and J.-P. Jouannaud, “Rewriting Systems,” in Handbook of Theoretical Computer Science, Vol.B: Formal Methods and Semantics, North-Holland, pp. 243-320, 1990.
-  E. Nantajeewarawat, K. Akama, and H. Koike, “Expanding Transformation: A Basis for Correctness Verification of Rewriting Rules,” Journal of Advanced Computational Intelligence and Intelligent Informatics, Vol.11, No.5, pp. 478-490, 2007.