Abstract
In most algebraic specification frameworks, the type system is restricted to sorts, subsorts, and first-order function types. This is in marked contrast to the so-called model-oriented frameworks, which provide higher-order types, interpreted set-theoretically as Cartesian products, function spaces, and power-sets. This paper presents a simple framework for algebraic specifications with higher-order types and set-theoretic models. It may be regarded as the basis for a Horn-clause approximation to the Z framework, and has the advantage of being amenable to prototyping and automated reasoning. Standard set-theoretic models are considered, and conditions are given for the existence of initial reducts of such models. Algebraic specifications for various set-theoretic concepts are considered.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
J. A. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operationsTheoretical Computer Science105217–2731992.
C. Hintermeier, H. Kirchner, and P. D. Mosses. Combining algebraic and set theoretic specifications. In M. Haveraaen, O. Owe, and O.-J. Dahl, editors Recent Trends in Data Type Specification, Proc. 11th Workshop on Specification of Abstract Data Types joint with the 9th general COMPASS workshop. Oslo, Norway, September 1995. Selected papers, volume 1130 of Lecture Notes in Computer Science, pages 255–273 Springer-Verlag, 1996.
K. Meinke. Universal algebra in higher types. Theoretical Computer Science, 100:385–4171992.
K. Meinke. Higher-order equational logic for specification, simulation and testing. In HOA’95, Proc. Second Int. Workshop on Higher-Order Algebra, Logic and Term Rewriting, volume 1074 of Lecture Notes in Computer Science, pages 124–143. Springer-Verlag, 1996.
J. Meseguer. Membership algebra as a semantic framework for equational specification. In Recent Trends in Algebraic Development Techniques, volume 1376 of Lecture Notes in Computer Science, pages18–61. Springer-Verlag, 1998.
P. D. Mosses. Unified algebras and institutions. In Proceedings 4th IEEE Symposium on Logic in Computer Science, Pacific Grove, pages 304–312 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kirchner, H., Mosses, P.D. (1998). Algebraic Specifications, Higher-Order Types and Set-Theoretic Models. In: Haeberer, A.M. (eds) Algebraic Methodology and Software Technology. AMAST 1999. Lecture Notes in Computer Science, vol 1548. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49253-4_27
Download citation
DOI: https://doi.org/10.1007/3-540-49253-4_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65462-9
Online ISBN: 978-3-540-49253-5
eBook Packages: Springer Book Archive