Skip to main content
SpringerLink
Log in
Book cover

International Conference of B and Z Users

ZB 2000: ZB 2000: Formal Specification and Development in Z and B pp 414–432Cite as

A Computation Model for Z Based on Concurrent Constraint Resolution

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1878))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Aiken and E. Wimmers. Solving systems of set constraints. In Symposium on Logic in Computer Science, pages 329–340, June 1992.

    Google Scholar 

  2. P. Arenas-Sanchez and A. Dovier. A minimality study for set unification. Journal of Functional and Logic Programming, 1997(7), 1997.

    Google Scholar 

  3. 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.

    Chapter  Google Scholar 

  4. R. Büssow and W. Grieskamp. The ZETA System Documentation. Technische Universität Berlin, Dec. 1998. URL: http://uebb.cs.tu-berlin.de/zeta.

    Google Scholar 

  5. 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.

    Google Scholar 

  6. 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.

    Google Scholar 

  7. M. Gordon and T. Melham, editors. Introduction to HOL: A theorem proving environment for higher-order logics. Cambridge University Press, 1993.

    Google Scholar 

  8. W. Grieskamp. The mZ calculus and its implementation. In Proceedings of the International Workshop on Implementation of Declarative Languages (IDL’99), Sept. 1999.

    Google Scholar 

  9. W. Grieskamp. A Set-Based Calculus and its Implementation. PhD thesis, Technische Universität Berlin, 1999.

    Google Scholar 

  10. M. Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19(20), 1994.

    Google Scholar 

  11. M. Hanus. A unified computation model for declarative programming. In Proc. of the 1997 Joint Conference on Declarative Programming, Grado (Italy), 1997.

    Google Scholar 

  12. M. Hanus. Curry-an integrated functional logic language. Technical report, Internet, 1999. Language report version 0.5.

    Google Scholar 

  13. 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.

    Google Scholar 

  14. B. Jayaraman and K. Moon. Subset logic programs and their implementation. Journal of Logic Programming, 19(20), 1999.

    Google Scholar 

  15. X. Jia. An approach to animating Z specifications. Internet: http://www.saturn.cs.depaul.edu/fm/zans.html, 1996.

  16. G. Kahn. Natural semantics. In Symposium on Theoretical Computer Science (STACS’97), volume 247 of Lecture Notes in Computer Science, 1987.

    Google Scholar 

  17. 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.

    Google Scholar 

  18. O. Owe. Partial logic reconsidered: A conservative approach. Formal Aspects of Computing, 5:208–223, 1997.

    Article  Google Scholar 

  19. 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.

    Google Scholar 

  20. J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992.

    Google Scholar 

  21. S. Valentine. The programming language Z—. Information and Software Technology, 37(5–6):293–301, May–June 1995.

    Google Scholar 

  22. D. H. D. Warren. The extended andorra model with implicit control. In ICLP’90 Parallel Logic Programming Workshop, 1990.

    Google Scholar 

  23. 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.

    Google Scholar 

  24. J. Wieland. A resolution algorithm for general subtyping constraints. Master’s thesis, Technische Universität Berlin, 1999.

    Google Scholar 

  25. M. Winikoff, P. Dart, and E. Kazmierczak. Rapid prototyping using formal specifications. In Proceedings of the Australasian Computer Science Conference, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Kommunikations- und Softwaretechnik Sekr. 5-13, Technische Universität Berlin FB13, Franklinstr. 28/29, D-10587, Berlin

    Wolfgang Grieskamp

Authors
  1. Wolfgang Grieskamp
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation