State-Transition Computation Models and Program Correctness Thereon

Abstract— A common framework for formalization of statetransition computation models is presented based on a general theory for studying the interrelationships between specifications, programs, computations, and program correctness. A necessary and sufficient condition for program correctness on this class of computation models is established. Application of the framework is demonstrated by formalizing as its instances two concrete examples of state-transition computation models, called the NAT computation model and the D-RULE computation model. A comparison between these two computation models as regards

• Type: Journal
• Year: 2007
• Where: JACIII
• Authors: Kiyoshi Akama, Ekawit Nantajeewarawat
• Keywords: Computation Models, JACIII 2007, Program Correctness, Statetransition Computation Models