A PROOF SYSTEM FOR CONDITIONAL ALGEBRAIC SPECIFICATIONS

被引：0

作者：

KOUNALIS, E ^{[1
]}

RUSINOWITCH, M ^{[1
]}

机构：

[1] INST NATL RECH INFORMAT & AUTOMAT LORRAINE, F-54600 VILLERS LES NANCY, FRANCE

来源：

LECTURE NOTES IN COMPUTER SCIENCE | 1991年 / 516卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Algebraic specifications provide a formal basis for designing data-structures and reasoning about their properties. Sufficient-completeness and consistency are fundamental notions for building algebraic specifications in a modular way. We give in this paper effective methods for testing these properties for specifications with conditional axioms.

引用

页码：51 / 63

页数：13

共 23 条

[1] TERMINATION OF REWRITING [J].

DERSHOWITZ, N .

JOURNAL OF SYMBOLIC COMPUTATION, 1987, 3 (1-2) :69-116

[2] COMPUTING WITH REWRITE SYSTEMS [J].

DERSHOWITZ, N .

INFORMATION AND CONTROL, 1985, 65 (2-3) :122-157

[3] PROVING TERMINATION WITH MULTI-SET ORDERINGS [J].

DERSHOWITZ, N ;

MANNA, Z .

COMMUNICATIONS OF THE ACM, 1979, 22 (08) :465-476

[4]

EHRIG H, 1978, LECTURE NOTES COMPUT, V62

[5]

GANZINGER H, 1987, LECT NOTES COMPUT SC, V247, P286

[6]

Goguen Joseph, 1978, TECHNICAL REPORT RC, VIV, P80

[7] PROOFS BY INDUCTION IN EQUATIONAL THEORIES WITH CONSTRUCTORS [J].

HUET, G ;

HULLOT, JM .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1982, 25 (02) :239-266

[8]

JOUANNAUD JP, 1986, 1ST P S LOG COMP SCI, P358

[9] ON SUFFICIENT-COMPLETENESS AND RELATED PROPERTIES OF TERM REWRITING-SYSTEMS [J].

KAPUR, D ;

NARENDRAN, P ;

ZHANG, H .

ACTA INFORMATICA, 1987, 24 (04) :395-415

[10]

KIRCHNER H, 1984, LECTURE NOTES COMPUT, P282

← 1 2 3 →