A Beginner’s Course on Reasoning About Imperative Programs

  • Kung-Kiu Lau
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3294)


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.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  2. 2.
    Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)Google Scholar
  3. 3.
    Barwise, J., Etchemendy, J.: The Language of First Order Logic, 3rd edn. CSLI (1993)Google Scholar
  4. 4.
    Extended Static Checking for Java Home Page,
  5. 5.
    Gries, D.: The Science of Programming. Springer, Heidelberg (1981)zbMATHGoogle Scholar
  6. 6.
    Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Addison-Wesley, Reading (1999)Google Scholar
  7. 7.
    The Java Modeling Language (JML) Home Page,
  8. 8.
    Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice Hall, Englewood Cliffs (1990)zbMATHGoogle Scholar
  9. 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. 10.
    Lau, K.-K.: CS1112: Reasoning about Programs,
  11. 11.
    Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley, Reading (1999)Google Scholar
  12. 12.
    SPARKAda, Praxis Critical Systems Limited,
  13. 13.
    Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)Google Scholar
  14. 14.

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Kung-Kiu Lau
    • 1
  1. 1.Department of Computer ScienceUniversity of ManchesterManchesterUnited Kingdom

Personalised recommendations