skip to main content
article

Experience teaching Z with tool and web support

Published:01 March 2001Publication History
Skip Abstract Section

Abstract

This short paper describes experiences of presenting the formal Z notation on one and later two course modules to computer science undergraduates, especially with respect to providing supporting web-based resources and using tool support. The modules were part of a more general course unit on formal methods.

References

  1. {BH97} J. P. Bowen and M. G. Hinchey. Formal models and the specification process. In A. B. Tucker, Jr., editor, The Computer Science and Engineering Handbook, chapter 107, pages 2302-2322. CRC Press, 1997. Section X, Software Engineering.Google ScholarGoogle Scholar
  2. {BH99} J. P. Bowen and M. G. Hinchey, editors. High-Integrity System Specification and Design. FACIT series. Springer-Verlag, 1999. Google ScholarGoogle Scholar
  3. {Bow96} J. P. Bowen. Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press, 1996.Google ScholarGoogle Scholar
  4. {Bow98} J. P. Bowen. An invoicing case study in Z. In M. Allemand, C. Attiogbé, and H. Habrias, editors, Comparing Systems Specification Techniques, pages 461-471, IRIN, 2 Rue de la Houssinière --- 44322, Nantes Cedex 3, France, 26-27 March 1998.Google ScholarGoogle Scholar
  5. {Bow00a} J. P. Bowen. The ethics of safety-critical systems. Communications of the ACM, 43(4):91-97, April 2000. Google ScholarGoogle Scholar
  6. {Bow00b} J. P. Bowen. Z: A formal specification notation. In M. Frappier and H. Habrias, editors, Software Specification Methods: An Overview Using a Case Study. Springer-Verlag, 2000. To appear. Google ScholarGoogle Scholar
  7. {DH96} C. N. Dean and M. G. Hinchey, editors. Teaching and Learning Formal Methods. Academic Press, 1996.Google ScholarGoogle Scholar
  8. {Fin96} K. Finney. Mathematical notation in formal specification: Too difficult for the masses? IEEE Transactions on Software Engineering, 22(2):158-159, February 1996. Google ScholarGoogle Scholar
  9. {Gar94} D. Garlan. Integrating formal methods into a professional master of software engineering program. In J. P. Bowen and J. A. Hall, editors, Z User Workshop, Cambridge 1994, Workshops in Computing, pages 71-85. Springer-Verlag, 1994.Google ScholarGoogle Scholar
  10. {Hal90} J. A. Hall. Seven myths of formal methods. IEEE Software, 7(5):11-19, September 1990. Google ScholarGoogle Scholar
  11. {HB99} M. G. Hinchey and J. P. Bowen, editors. Industrial-Strength Formal Methods in Practice. FACIT series. Springer-Verlag, 1999.Google ScholarGoogle Scholar
  12. {HJ89} I. J. Hayes and C. B. Jones. Specifications are not (necessarily) executable. IEE/BCS Software Engineering Journal, 4(6):330-338, November 1989. Google ScholarGoogle Scholar
  13. {Jac97} J. Jacky. The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, 1997. Google ScholarGoogle Scholar
  14. {Kin90} P. King. Printing Z and Object-Z LATEX documents. Department of Computer Science, University of Queensland, St. Lucia 4072, Australia, May 1990.Google ScholarGoogle Scholar
  15. {Lam93} L. Lamport. LATEX User's Guide & Reference Manual: A document preparation system. Addison-Wesley Publishing Company, 2nd edition, 1993. Google ScholarGoogle Scholar
  16. {LaT99} LaTeX3 Project. LATEX: A document preparation system, 8 November 1999. URL: http://www.latex-project.org/Google ScholarGoogle Scholar
  17. {Nic91} J. E. Nicholls. A survey of Z courses in the UK. In J. E. Nicholls, editor, Z User Workshop, Oxford 1990, Workshops in Computing, pages 343-350. Springer-Verlag, 1991. Google ScholarGoogle Scholar
  18. {Nis99} N. Nissanke. Introductory Logic and Sets for Computer Scientists. Addison Wesley Longman, 1999. Google ScholarGoogle Scholar
  19. {PST96} B. F. Potter, J. E. Sinclair, and D. Till. An Introduction to Formal Specification and Z. Prentice Hall International Series in Computer Science, 2nd edition, 1996. Google ScholarGoogle Scholar
  20. {Sai92} H. Saiedian. Mathematics of computing. Journal of Computer Science Education, 3(3):203-221, 1992.Google ScholarGoogle Scholar
  21. {Sch00} C. Schenk. MiKTEX: Free TeX for Windows users, 8 July 2000. URL: http://www.miktex.org/Google ScholarGoogle Scholar
  22. {Som95} I. Sommerville. Model-based specification. In Software Engineering, chapter 9, pages 189-205. Addison-Wesley Publishing Company, 5th edition, 1995.Google ScholarGoogle Scholar
  23. {Spi92a} J. M. Spivey. The fUZZ Manual. Computing Science Consultancy, 34 Westlands Grove, Stockton Lane, York YO3 0EF, UK, 2nd edition, July 1992.Google ScholarGoogle Scholar
  24. {Spi92b} J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992. Google ScholarGoogle Scholar
  25. {SVR98} SVRC. Object-Z LaTeX macros. The University of Queensland, Australia, 25 February 1998. URL: http://svrc.it.uq.edu.au/Object-Z/pages/latex.htmlGoogle ScholarGoogle Scholar
  26. {WD96} J. C. P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science, 1996. Google ScholarGoogle Scholar
  27. {Xia95} Xiaoping Jia. An approach to animating Z specifications. In Proc. 19th Annual IEEE International Computer Software and Applications Conference (COMPSAC'95), pages 108-113, Dallas, Texas, USA, August 1995. Google ScholarGoogle Scholar
  28. {Xia98a} Xiaoping Jia. A tutorial of ZANS --- a Z animation tool. Release 0.31, July 1998.Google ScholarGoogle Scholar
  29. {Xia98b} Xiaoping Jia. Z animations. DePaul University, USA, 25 February 1998. URL: http://sotiris.cs.depaul.edu/fm/zans.htmlGoogle ScholarGoogle Scholar
  30. {Xia98c} Xiaoping Jia. Z type checker. DePaul University, USA, 12 August 1998. URL: http://sotiris.cs.depaul.edu/fm/ztc.htmlGoogle ScholarGoogle Scholar
  31. {Xia98d} Xiaoping Jia. ZTC: A Type Checker for Z Notation --- User's Guide. Version 2.03. DePaul University, Institute for Software Engineering, Department of Computer Science and Information Systems, Chicago, Illinois, USA, August 1998.Google ScholarGoogle Scholar

Index Terms

  1. Experience teaching Z with tool and web support
    Index terms have been assigned to the content through auto-classification.

    Recommendations

    Comments

    Login options

    Check if you have access through your login credentials or your institution to get full access on this article.

    Sign in

    Full Access

    • Published in

      cover image ACM SIGSOFT Software Engineering Notes
      ACM SIGSOFT Software Engineering Notes  Volume 26, Issue 2
      March 2001
      76 pages
      ISSN:0163-5948
      DOI:10.1145/505776
      Issue’s Table of Contents

      Copyright © 2001 Author

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      • Published: 1 March 2001

      Check for updates

      Qualifiers

      • article

    PDF Format

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader