Abstract
We present a computation model for Z, which is based on a reduction to a small calculus, called μZ, and on concurrent constraint resolution techniques applied for computing in this calculus. The power of the model is comparable to that of functional logic languages, and combines the strength of higher-order functional computation with logic computation. The model is implemented as part of the ZETA system, where it is used for executing Z specifications for the purpose of testdata evaluation and prototyping.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Aiken and E. Wimmers. Solving systems of set constraints. In Symposium on Logic in Computer Science, pages 329–340, June 1992.
P. Arenas-Sanchez and A. Dovier. A minimality study for set unification. Journal of Functional and Logic Programming, 1997(7), 1997.
R. D. Arthan. Recursive definitions in Z. In J. P. Bowen, A. Fett, and M. G. Hinchey, editors, ZUM’98: The Z Formal Specification Notation, volume 1493 of Lecture Notes in Computer Science, pages 154–171. Springer-Verlag, 1998.
R. Büssow and W. Grieskamp. The ZETA System Documentation. Technische Universität Berlin, Dec. 1998. URL: http://uebb.cs.tu-berlin.de/zeta.
R. Büssow and W. Grieskamp. A Modular Framework for the Integration of Heterogenous Notations and Tools. In K. Araki, A. Galloway, and K. Taguchi, editors, Proc. of the 1st Intl.Conference on Integrated Formal Methods-IFM’99. Springer-Verlag, London, June 1999.
H. S. Goodman. The Z-into-Haskell tool-kit: An illustrative case study. In J. P. Bowen and M. G. Hinchey, editors, ZUM’95: The Z Formal Specification Notation, volume 967 of Lecture Notes in Computer Science, pages 374–388. Springer-Verlag, 1995.
M. Gordon and T. Melham, editors. Introduction to HOL: A theorem proving environment for higher-order logics. Cambridge University Press, 1993.
W. Grieskamp. The mZ calculus and its implementation. In Proceedings of the International Workshop on Implementation of Declarative Languages (IDL’99), Sept. 1999.
W. Grieskamp. A Set-Based Calculus and its Implementation. PhD thesis, Technische Universität Berlin, 1999.
M. Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19(20), 1994.
M. Hanus. A unified computation model for declarative programming. In Proc. of the 1997 Joint Conference on Declarative Programming, Grado (Italy), 1997.
M. Hanus. Curry-an integrated functional logic language. Technical report, Internet, 1999. Language report version 0.5.
P. H. Hartel, M. Feeley, M. Alt, L. Augustsson, P. Baumann, M. Beemster, E. Chailloux, C. H. Flood, W. Grieskamp, J. H. G. van Groningen, K. Hammond, B. Hausman, M. Y. Ivory, R. E. Jones, J. Kamperman, P. Lee, X. Leroy, R. D. Lins, S. Loosemore, N. Röjemo, M. Serrano, J.-P. Talpin, J. Thackray, S. Thomas, P. Walters, P. Weis, and P. Wentworth. Benchmarking implementations of functional languages with “pseudoknot”, a Float-Intensive benchmark. J. of Functional Programming, 6(4), 1996.
B. Jayaraman and K. Moon. Subset logic programs and their implementation. Journal of Logic Programming, 19(20), 1999.
X. Jia. An approach to animating Z specifications. Internet: http://www.saturn.cs.depaul.edu/fm/zans.html, 1996.
G. Kahn. Natural semantics. In Symposium on Theoretical Computer Science (STACS’97), volume 247 of Lecture Notes in Computer Science, 1987.
M. Mehl, R. Scheidhauer, and C. Schulte. An Abstract Machine for Oz. Research Report RR-95-08, Deutsches Forschungszentrum für Künstliche Intelligenz, Stuhl-satzenhausweg 3, D66123 Saarbrücken, Germany, June 1995. Also in: Proceedings ofPLILP’95, Springer-Verlag, LNCS, Utrecht, The Netherlands.
O. Owe. Partial logic reconsidered: A conservative approach. Formal Aspects of Computing, 5:208–223, 1997.
G. Smolka. A calculus for higher-order concurrent constraint programming with deep guards. Research Report RR-94-03, Deutsches Forschungszentrum für Künstliche Intelligenz, Stuhlsatzenhausweg 3, D-66123 Saarbrücken, Germany, Feb. 1994.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992.
S. Valentine. The programming language Z—. Information and Software Technology, 37(5–6):293–301, May–June 1995.
D. H. D. Warren. The extended andorra model with implicit control. In ICLP’90 Parallel Logic Programming Workshop, 1990.
M. M. West and B. M. Eaglestone. Software development: Two approaches to animation of Z specifications using Prolog. IEE/BCS Software Engineering Journal, 7(4):264–276, July 1992.
J. Wieland. A resolution algorithm for general subtyping constraints. Master’s thesis, Technische Universität Berlin, 1999.
M. Winikoff, P. Dart, and E. Kazmierczak. Rapid prototyping using formal specifications. In Proceedings of the Australasian Computer Science Conference, 1998.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grieskamp, W. (2000). A Computation Model for Z Based on Concurrent Constraint Resolution. In: ZB 2000: Formal Specification and Development in Z and B. ZB 2000. Lecture Notes in Computer Science, vol 1878. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44525-0_24
Download citation
DOI: https://doi.org/10.1007/3-540-44525-0_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67944-8
Online ISBN: 978-3-540-44525-8
eBook Packages: Springer Book Archive