Top > JACIII > State-Transition Computation Models and Program Correctness Th ...

single-jc.php

JACIII Vol.11 No.10 pp. 1250-1261
doi: 10.20965/jaciii.2007.p1250
(2007)

Paper:

Views over last 60 days: 484

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

Received:
October 30, 2006
Accepted:
February 1, 2007
Published:
December 20, 2007
Creative Commons License
Keywords:
state-transition computation model, program correctness, embedding mapping
Abstract
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.
Cite this article as:
K. Akama and E. Nantajeewarawat, “State-Transition Computation Models and Program Correctness Thereon,” J. Adv. Comput. Intell. Intell. Inform., Vol.11 No.10, pp. 1250-1261, 2007.
Data files:
References
  1. [1] 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.
  2. [2] J. W. Lloyd, “Foundations of Logic Programming,” second, extended edition, Springer-Verlag, 1987.
  3. [3] T. Frühwirth, “Theory and Practice of Constraint Handling Rules,” Journal of Logic Programming, Vol.37, pp. 95-138, 1998.
  4. [4] 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.
  5. [5] R. Bird, “Introduction to Functional Programming,” second edition, Prentice Hall, 1998.
  6. [6] 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.
  7. [7] 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.
  8. [8] Y. Gurevich, “Sequential Abstract-State Machines Capture Sequential Algorithms,” ACM Transactions on Computational Logic, Vol.1, No.1, pp. 77-111, 2000.
  9. [9] E. Börger and R. Stärk, “Abstract State Machines: A Method for High-level System Design and Analysis,” Springer-Verlag, 2003.
  10. [10] C. A. Petri, “Nets, Times and Spaces,” Theoretical Computer Science, Vol.153, pp. 3-48, 1996.
  11. [11] 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.
  12. [12] 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.

Creative Commons License  This article is published under a Creative Commons Attribution-NoDerivatives 4.0 Internationa License.

*This site is desgined based on HTML5 and CSS3 for modern browsers, e.g. Chrome, Firefox, Safari, Edge, Opera.

Last updated on Dec. 13, 2024