A Beginner’s Course on Reasoning About Imperative Programs
- 280 Downloads
Formal Methods teaching at undergraduate level has been going on at Manchester for a good number of years. We have introduced various courses based on different approaches. We have experienced the usual problems. To combat these problems, our approaches and our course contents have evolved accordingly over the years. In this paper we briefly trace this evolution, and describe the latest course, on reasoning about simple imperative programs, for first-year students who are half-way through our introductory programming course.
Unable to display preview. Download preview PDF.
- 2.Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)Google Scholar
- 3.Barwise, J., Etchemendy, J.: The Language of First Order Logic, 3rd edn. CSLI (1993)Google Scholar
- 4.Extended Static Checking for Java Home Page, http://research.compaq.com/SRC/esc/
- 6.Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Addison-Wesley, Reading (1999)Google Scholar
- 7.The Java Modeling Language (JML) Home Page, http://www.cs.iastate.edu/~leavens/JML.html
- 9.Latham, J.T., Bush, V.J., Cottam, I.D.: The Programming Process: An Introduction using VDM and Pascal. Addison-Wesley, Reading (1990)Google Scholar
- 10.Lau, K.-K.: CS1112: Reasoning about Programs, http://www.cs.man.ac.uk/~kung-kiu/cs1112/
- 11.Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley, Reading (1999)Google Scholar
- 12.SPARKAda, Praxis Critical Systems Limited, http://www.praxis-cs.co.uk/sparkada/
- 13.Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)Google Scholar
- 14.Tarski’s World, http://wwwcsli.stanford.edu/hp/Tarski1.html