
Consistency and Semantics of Equational Definitions over Predefined Algebras
Author(s) -
Valentin M. Antimirov,
Anatoli Degtyarev
Publication year - 1993
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v22i431.6747
Subject(s) - correctness , consistency (knowledge bases) , algebraic specification , semantics (computer science) , programming language , computer science , algebraic number , algebra over a field , algebraic semantics , theoretical computer science , mathematics , formal specification , pure mathematics , artificial intelligence , mathematical analysis
We introduce and study the notion of an equational definition over a predefined algebra (EDPA) which is a modification of the notion of an algebraic specification enrichment. We argue that the latter is not quite appropriate when dealing with partial functions (in particular, with those defined by non-terminating functional programs), and suggest EDPA as a more adequate tool for specification and verification purposes. Several results concerning consistency of enrichments and correctness of EDPA are presented. The relations between EDPA and some other approaches to algebraic specification of partial functions are discussed.