Abstract
Z is a well-defined and well-known specification language. Unfortunately, it takes significant expertise to use existing tools (such as theorem provers) to automatically check properties of Z specifications. Because Alloy is substantially similar to Z and the Alloy Analyzer offers a relatively simple method of model checking, we believe that Alloy should be largely employed in classes that teach Z. To this end, we present an online tutorial especially designed to help students transition from Z to Alloy. The tutorial includes both the classic Birthday Book example and a large real-world scenario based on a Kitchen Environment. Our experiences with novices studying the tutorial suggest that the tutorial helps students learn both Z and Alloy. In addition, novices can answer questions correctly about the approximately 500-line Kitchen Environment model after only a few hours of study.
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
Alloy Analyzer 4, http://alloy.mit.edu/alloy4/ (2009-07-15)
Alloy FAQ, http://alloy.mit.edu/faq.php (2009-07-15)
Brakman, H., Driessen, V., Kavuma, J., Bijvank, L.N., Vermolen, S.: Supporting Formal Method Teaching with Real-Life Protocols. In: Formal Methods in the Teaching Lab: Examples, Cases, Assignments and Projects Enhancing Formal Methods Education, pp. 59–68. McMaster University, Canada (2006)
Broda, K., Ma, J., Sinnadurai, G., Summers, A.: Friendly e-tutor for Natural Deduction. In: TFM: Practice and Experience. BCS-FACS, London (2006)
Dean, N.: Development of an Interactive Case e-Study. In: TFM: Practice and Experience Workshop, pp. 13–20. BCS-FACS, Oxford Brookes University (2003)
deBry, R.: Learning exercises for the rest of the brain. J. Comput. Small Coll. 20(1), 291–296 (2004)
Duke, R., Miller, T., Strooper, P.: Integrating Formal Specification and Software Verification and Validation. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 124–139. Springer, Heidelberg (2004)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)
Jonathan, J.: The way of Z: Practical programming with formal methods. Cambridge University Press, NY (1996)
Kolb, D.A.: Experiential learning: Experience as the source of learning and development. Prentice-Hall, Englewood Cliffs (1984)
Larsen, P.G.: Two courses on VDM++ for Embedded Systems: Learning by Doing. In: Formal Methods in the Teaching Lab: Examples, Cases, Assignments and Projects Enhancing Formal Methods Education, Canada, pp. 21–26 (2006)
Lightfoot, D.: Voici les votes! – formal specification as light entertainment: An example of audience participation in developing a specification. In: TFM: Practice and Experience Workshop, pp. 71–75. BCS-FACS, Oxford Brookes U. (2003)
Mandrioli, D.: Advertising Formal Methods and Organizing Their Teaching: Yes, but... In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 214–224. Springer, Heidelberg (2004)
Martin, J.M.: Teaching Formal Methods: An Industrial Perspective. In: TFM: Practice and Experience Workshop, pp. 35–39. BCS-FACS, Oxford Brookes U. (2003)
Montessori, M.: The Montessori Method, Schocken (1988)
Pepper, P.: Distributed Teaching of Formal Methods. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 140–152. Springer, Heidelberg (2004)
Piaget, J., Mays, W., Beth, E.W.: Mathematical Epistemology and Psychology. D. Reidel Publishing Company, Dordrecht-Netherlands (1966)
Piaget, J., Garcia, R.: Psychogenesis and the History of Sciences. Columbia University Press, New York (1980)
Reed, J.N., Sinclair, J.E.: Motivating Study of Formal Methods in the Classroom. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 32–46. Springer, Heidelberg (2004)
Rosa, S.: Designing Algorithms in High School Mathematics. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 17–31. Springer, Heidelberg (2004)
Rudall, J.: From Z to SPIN in One Module. In: TFM: Practice and Experience Workshop, pp. 71–75. BCS-FACS, Oxford Brookes U. (2003)
Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International, UK (1992)
Tarkan, S.: The Formal Specification of a Kitchen Environment. Master’s scholarly paper, University of Maryland (2009)
TEX to HTML translator, http://hutchinson.belmont.ma.us/tth/ (2009-07-15)
The Promela Language, http://en.wikipedia.org/wiki/Promela (2009-07-15)
The SPIN Model Checker, http://spinroot.com/ (2009-07-15)
Woodcock, J., Davies, J.: Using Z: specification, refinement, and proof. Prentice-Hall, Upper Saddle River (1996)
Z to Alloy Tutorial, http://ztoalloy.cs.umd.edu/ (2009-07-15)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tarkan, S., Sazawal, V. (2009). Chief Chefs of Z to Alloy: Using a Kitchen Example to Teach Alloy with Z. In: Gibbons, J., Oliveira, J.N. (eds) Teaching Formal Methods. TFM 2009. Lecture Notes in Computer Science, vol 5846. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04912-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-04912-5_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04911-8
Online ISBN: 978-3-642-04912-5
eBook Packages: Computer ScienceComputer Science (R0)