ITEM METADATA RECORD
Title: Proving semantical equivalence of data specifications
Authors: Piessens, Frank ×
Steegmans, Eric #
Issue Date: Mar-1997
Publisher: Elsevier science bv
Series Title: Journal of Pure and Applied Algebra vol:116 issue:1-3 pages:291-322
Abstract: More than two decades ago, Peter Freyd introduced essentially algebraic specifications, a well-behaved generalization of algebraic specifications, allowing for equational partiality. These essentially algebraic specifications turn out to have a number of very interesting applications in computer science. In this paper, we present a deduction system for essentially algebraic specifications that is very suitable as the underlying deduction system of an automated theorem prover. Using the well-known fact that theories of sketches can be constructed as initial algebras of essentially algebraic specifications, we describe a semi-automatic procedure for proving the equivalence of the theories of two sketches. Next, we demonstrate that sketches are a very suitable formalism for making semantic data specifications, as used in database design and software engineering. Two such data specifications are semantically equivalent iff their model categories in FinSet are equivalent. Equivalence of theories is a sufficient condition for semantical equivalence, and hence the procedure to prove the equivalence of the theories of sketches can be used as a powerful tool to prove semantical equivalence of data specifications. Proving semantical equivalence of data specifications is an important component of the view integration process, i.e. the process of integrating a number of partly overlapping data specifications into one large data specification. (C) 1997 Elsevier Science B.V.
URI: 
ISSN: 0022-4049
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:

There are no files associated with this item.

Request a copy

 




All items in Lirias are protected by copyright, with all rights reserved.

© Web of science