MONSTR II - Suspending Semantics and Independence

Richard Banach (Computer Science Dept., Manchester University, UK)

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, MONSTR, Semantic Models, Term Graph Rewriting

Categories: D.1.3, D.3.1, F.3.2, F.4.2