Skip to main content
SpringerLink
Log in
Book cover

Formal Methods Teaching Workshop

FMTea 2019: Formal Methods Teaching pp 3–20Cite as

Logic, Algebra, and Geometry at the Foundation of Computer Science

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11758))

Abstract

This paper shows by examples how the Theory of Programming can be taught to first-year CS undergraduates. The only prerequisite is their High School acquaintance with algebra, geometry, and propositional calculus. The main purpose of teaching the subject is to support practical programming assignments and projects throughout the degree course. The aims would be to increase the student’s enjoyment of programming, reduce the workload, and increase the prospect of success.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Infer static analyzer website: https://fbinfer.com.

  2. 2.

    Course link: https://vtss.doc.ic.ac.uk/teaching/InferLab.html.

References

  1. Back, R.-J.: Invariant based programming: basic approach and teaching experiences. Formal Asp. Comput. 21(3), 227–244 (2009)

    Article  Google Scholar 

  2. Back, R.-J., Eriksson, J., Mannila, L.: Teaching the construction of correct programs using invariant based programming. In: Proceedings of the 3rd South-East European Workshop on Formal Methods (2007)

    Google Scholar 

  3. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_3

    Chapter  Google Scholar 

  4. Bird, R.: Pearls of Functional Algorithm Design. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

  5. Bird, R., De Moor, O.: The algebra of programming. In: NATO ASI DPD, pp. 167–203 (1996)

    Google Scholar 

  6. Boole, G.: An Investigation of the Laws of Thought: On Which Are Founded the Mathematical Theories of Logic and Probabilities. Dover Publications, New York (1854)

    MATH  Google Scholar 

  7. Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 459–465. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_33

    Chapter  Google Scholar 

  8. Davis, M.: Engines of Logic: Mathematicians and the Origin of the Computer. WW Norton & Co., Inc., New York (2001)

    MATH  Google Scholar 

  9. Ferreira, J.F., Mendes, A.: Students’ feedback on teaching mathematics through the calculational method. In: 2009 39th IEEE Frontiers in Education Conference, pp. 1–6. IEEE (2009)

    Google Scholar 

  10. Ferreira, J.F., Mendes, A., Backhouse, R., Barbosa, L.S.: Which mathematics for the information society? In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 39–56. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_4

    Chapter  Google Scholar 

  11. Ferreira, J.F., et al.: Logic training through algorithmic problem solving. In: Blackburn, P., van Ditmarsch, H., Manzano, M., Soler-Toscano, F. (eds.) TICTTL 2011. LNCS (LNAI), vol. 6680, pp. 62–69. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21350-2_8

    Chapter  Google Scholar 

  12. Flanagan, C., et al.: Extended static checking for Java. ACM SIGPLAN Not. 37(5), 234–245 (2002)

    Article  Google Scholar 

  13. Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21–41. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-14806-9_2

    Chapter  Google Scholar 

  14. Antony, C., Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  Google Scholar 

  15. Hoare, T., Struth, G., Woodcock, J.: A calculus of space, time, and causality: its algebra, geometry, logic. In: Ribeiro, P., Sampaio, A. (eds.) UTP 2019. LNCS, vol. 11885, pp. 3–21. Springer, Cham (2019)

    Google Scholar 

  16. Hutton, G.: Programming in Haskell. Cambridge University Press, Cambridge (2016)

    Book  Google Scholar 

  17. Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. (TOSEM) 11(2), 256–290 (2002)

    Article  Google Scholar 

  18. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20

    Chapter  MATH  Google Scholar 

  19. Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10235-3

    Book  MATH  Google Scholar 

  20. Milner, R.: Communicating and Mobile Systems: The Pi Calculus. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  21. Morgan, C.: (In-)formal methods: the lost art. In: Liu, Z., Zhang, Z. (eds.) SETSS 2014. LNCS, vol. 9506, pp. 1–79. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-29628-9_1

    Chapter  Google Scholar 

  22. de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26

    Chapter  Google Scholar 

  23. O’Hearn, P.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)

    Article  MathSciNet  Google Scholar 

  24. O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_1

    Chapter  Google Scholar 

  25. William of Ockham: Ockham’s Theory of Propositions: Part II of the Summa Logicae. University of Notre Dame Press (1980). Translated by Alfred J. Freddoso and Henry Schuurman

    Google Scholar 

  26. Oliveira, J.N., Ferreira, M.A.: Alloy meets the algebra of programming: a case study. IEEE Trans. Softw. Eng. 39(3), 305–326 (2012)

    Article  Google Scholar 

  27. Papadimitriou, C.H.: Computational Complexity. Wiley, Hoboken (2003)

    MATH  Google Scholar 

  28. Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 238–248. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02654-1_13

    Chapter  Google Scholar 

  29. Pedersen, J.B., Welch, P.H.: The symbiosis of concurrency and verification: teaching and case studies. Formal Asp. Comput. 30(2), 239–277 (2018)

    Article  MathSciNet  Google Scholar 

  30. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74. IEEE (2002)

    Google Scholar 

  31. Sasse, R., Meseguer, J.: Java+ ITP: a verification tool based on Hoare logic and algebraic semantics. Electron. Notes Theor. Comput. Sci. 176(4), 29–46 (2007)

    Article  Google Scholar 

  32. Smith, R.: Prior Analytics. Hackett Publishing, Indianapolis (1989)

    Google Scholar 

  33. Vazou, N., Breitner, J., Kunkel, R., Van Horn, D., Hutton, G.: Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). In: Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, pp. 132–144. ACM (2018)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Cambridge, UK

    Tony Hoare

  2. Cambridge University Computing Laboratory, Cambridge, UK

    Tony Hoare

  3. HASLab, INESC TEC, Porto, Portugal

    Alexandra Mendes

  4. Department of Informatics, Universidade da Beira Interior, Covilhã, Portugal

    Alexandra Mendes

  5. INESC-ID & Instituto Superior Técnico, University of Lisbon, Lisbon, Portugal

    João F. Ferreira

Authors
  1. Tony Hoare
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexandra Mendes
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. João F. Ferreira
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to João F. Ferreira .

Editor information

Editors and Affiliations

  1. University of Surrey, Guildford, UK

    Brijesh Dongol

  2. Åbo Akademi University, Turku, Finland

    Luigia Petre

  3. The University of Queensland, Brisbane, QLD, Australia

    Graeme Smith

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Hoare, T., Mendes, A., Ferreira, J.F. (2019). Logic, Algebra, and Geometry at the Foundation of Computer Science. In: Dongol, B., Petre, L., Smith, G. (eds) Formal Methods Teaching. FMTea 2019. Lecture Notes in Computer Science(), vol 11758. Springer, Cham. https://doi.org/10.1007/978-3-030-32441-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32441-4_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32440-7

  • Online ISBN: 978-3-030-32441-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation