On equality predicates in algebraic specification languages

被引：0

作者：

Masaki, Nakamura ^{[1
]}

Kokichi, Futatsugi ^{[1
]}

机构：

[1] Japan Adv Inst Sci & Technol, Sch Informat Sci, Tokyo, Japan

来源：

THEORETICAL ASPECTS OF COMPUTING - ICTAC 2007, PROCEEDINGS | 2007年 / 4711卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：381 / +

页数：3

共 10 条

[1]

[Anonymous], 2003, Cambridge Tracts in Theoretical Computer Science, V55

[2]

BURSTALL RM, 1980, LECTURE NOTES COMPUT, V86, P292, DOI DOI 10.1007/3-540-10007-5_41

[3]

Diaconescu R, 1998, AMAST SERIES COMPUTI, V6

[4]

FUTATSUGI K, 1985, P 12 ACM S PRINC PRO, P52

[5]

Giesl R, 2004, LECT NOTES COMPUT SC, V3091, P210

[6]

Goguen J., 1996, Algebraic Semantics of Imperative Programs, DOI DOI 10.7551/MITPRESS/1188.001.0001

[7]

GOGUEN JA, 2000, SOFTWARE ENG OBJ ALG

[8]

Meinke K., 1992, HDB LOGIC COMPUTER S, VI, P189

[9]

Ohlebusch Enno, 2002, Advanced Topics in Term Rewriting

[10]

WIRSING M, 1990, FORMAL MODELS SEMANT, P675

← 1 →