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.
- {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 Scholar
- {BH99} J. P. Bowen and M. G. Hinchey, editors. High-Integrity System Specification and Design. FACIT series. Springer-Verlag, 1999. Google Scholar
- {Bow96} J. P. Bowen. Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press, 1996.Google Scholar
- {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 Scholar
- {Bow00a} J. P. Bowen. The ethics of safety-critical systems. Communications of the ACM, 43(4):91-97, April 2000. Google Scholar
- {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 Scholar
- {DH96} C. N. Dean and M. G. Hinchey, editors. Teaching and Learning Formal Methods. Academic Press, 1996.Google Scholar
- {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 Scholar
- {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 Scholar
- {Hal90} J. A. Hall. Seven myths of formal methods. IEEE Software, 7(5):11-19, September 1990. Google Scholar
- {HB99} M. G. Hinchey and J. P. Bowen, editors. Industrial-Strength Formal Methods in Practice. FACIT series. Springer-Verlag, 1999.Google Scholar
- {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 Scholar
- {Jac97} J. Jacky. The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, 1997. Google Scholar
- {Kin90} P. King. Printing Z and Object-Z LATEX documents. Department of Computer Science, University of Queensland, St. Lucia 4072, Australia, May 1990.Google Scholar
- {Lam93} L. Lamport. LATEX User's Guide & Reference Manual: A document preparation system. Addison-Wesley Publishing Company, 2nd edition, 1993. Google Scholar
- {LaT99} LaTeX3 Project. LATEX: A document preparation system, 8 November 1999. URL: http://www.latex-project.org/Google Scholar
- {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 Scholar
- {Nis99} N. Nissanke. Introductory Logic and Sets for Computer Scientists. Addison Wesley Longman, 1999. Google Scholar
- {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 Scholar
- {Sai92} H. Saiedian. Mathematics of computing. Journal of Computer Science Education, 3(3):203-221, 1992.Google Scholar
- {Sch00} C. Schenk. MiKTEX: Free TeX for Windows users, 8 July 2000. URL: http://www.miktex.org/Google Scholar
- {Som95} I. Sommerville. Model-based specification. In Software Engineering, chapter 9, pages 189-205. Addison-Wesley Publishing Company, 5th edition, 1995.Google Scholar
- {Spi92a} J. M. Spivey. The fUZZ Manual. Computing Science Consultancy, 34 Westlands Grove, Stockton Lane, York YO3 0EF, UK, 2nd edition, July 1992.Google Scholar
- {Spi92b} J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992. Google Scholar
- {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 Scholar
- {WD96} J. C. P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science, 1996. Google Scholar
- {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 Scholar
- {Xia98a} Xiaoping Jia. A tutorial of ZANS --- a Z animation tool. Release 0.31, July 1998.Google Scholar
- {Xia98b} Xiaoping Jia. Z animations. DePaul University, USA, 25 February 1998. URL: http://sotiris.cs.depaul.edu/fm/zans.htmlGoogle Scholar
- {Xia98c} Xiaoping Jia. Z type checker. DePaul University, USA, 12 August 1998. URL: http://sotiris.cs.depaul.edu/fm/ztc.htmlGoogle Scholar
- {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 Scholar
Index Terms
- Experience teaching Z with tool and web support
Recommendations
Teaching style, ICT experience and teachers' attitudes toward teaching with Web 2.0
Emphasis on 21st Century Skills development has increased expectations on teachers to take advantages of emerging technologies to support student learning. Yet it is not clear whether teachers are well equipped with the necessary skills, support, and ...
Customizing a Field Experience for CS Undergrads in Teaching Computer Science for Your School Context: (Abstract Only)
SIGCSE '18: Proceedings of the 49th ACM Technical Symposium on Computer Science EducationThis workshop's goal is to help faculty who want to establish a course (or alternate vehicle) for mentoring undergraduates with some CS background to participate in K-12 teaching CS in local schools with engaging pedagogy. The workshop leverages the ...
Comments