On equality predicates in algebraic specification languages
On equality predicates in algebraic specification languages
复制标题
DOI：
10.1007/978-3-540-75292-9_26
复制
发表时间：
2007-09
期刊：
影响因子：
--
通讯作者：
Nakamura Masaki;Futatsugi Kokichi
中科院分区：
文献类型：
--
作者：
Nakamura Masaki;Futatsugi Kokichi
OBJ 代数规范语言的执行基于术语重写系统 (TRS)，这是执行方程推理的有效理论。我们重点关注 OBJ 语言中实现的相等谓词。相等谓词用于通过 TRS 测试给定术语的相等性。不幸的是，众所周知，当前带有等式谓词的 OBJ 语言的执行引擎并不健全。为了解决这个问题，我们定义了一个适用于OBJ语言模块系统的模块化术语重写系统（MTRS），并提出了一种基于MTRS的新的等式谓词。
The execution of OBJ algebraic specification languages is based on the term rewriting system (TRS), which is an efficient theory to perform equational reasoning. We focus on the equality predicate implemented in OBJ languages. The equality predicate is used to test the equality of given terms by TRS. Unfortunately, it is well known that the current execution engine of OBJ languages with the equality predicate is not sound. To solve this problem, we define a modular term rewriting system (MTRS), which is suitable for the module system of OBJ languages, and propose a new equality predicate based on MTRS.