Semantic foundations for generalized rewrite theories

作     者：Bruni, Roberto Meseguer, Jose 

作者机构：Univ Pisa Dipartimento Informat I-56127 Pisa Italy Univ Illinois CS Dept Urbana IL 61801 USA 

出 版 物：《THEORETICAL COMPUTER SCIENCE》 (理论计算机科学)

年 卷 期：2006年第360卷第1-3期

页      面：386-414页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：FET-GC, (IST-2001-32747) Office of Naval Research, ONR, (N00014-02-1-0715) Ministero dell’Istruzione, dell’Università e della Ricerca, MIUR, (2001013518) 

主　　题：conditional rewriting logic membership equational logic contextual rewrites semantics 

摘      要：Rewriting logic (RL) is a logic of actions whose models are concurrent systems. Rewrite theories involve the specification of equational theories of data and state structures together with a set of rewrite rules that model the dynamics of concurrent systems. Since its introduction, more than one decade ago, RL has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. These extensions may develop along several dimensions, like the choice of the underlying equational logic, the kind of side conditions allowed in rewrite rules and operational concerns for the execution of certain rewrites. In particular, the Maude system now supports subsorting and conditional sentences in the equational logic for data, and also frozen arguments to block undesired nested rewrites;moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories. Our results provide a mathematical semantics for Maude, and a foundation for formal reasoning about Maude specifications. (C) 2006 Elsevier B.V. All rights reserved.