JUCS - Journal of Universal Computer Science 3(7): 756-802, doi: 10.3217/jucs-003-07-0756
MONSTR II - Suspending Semantics and Independence
expand article infoRichard Banach
‡ Computer Science Dept., Manchester University, Manchester, United Kingdom
Open Access
Abstract
The suspending semantic model for the execution of the MONSTR generali sed term graph rewriting language is defined. This is the canonical operational semantic model for the MONSTR language. Its correctness with respect to DACTL semantics is discussed, a nd a number of general theorems on the soundness of suspending executions with respec t to DACTL semantics are proved. General theorems are proved about the independence of susp ending primitive actions, which are useful in the verification of MONSTR systems.
Keywords
Intermediate Languages, Term Graph Rewriting, MONSTR, Semantic Models