Teaching How to Derive Correct Concurrent Programs from State-Based Specifications and Code Patterns

  • Manuel Carro
  • Julio Mariño
  • Ángel Herranz
  • Juan José Moreno-Navarro
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3294)


The fun of teaching and learning concurrent programming is sometimes darkened by the difficulty in getting concurrent programs to work right. In line with other programming subjects in our department, we advocate the use of formal specifications to state clearly how a concurrent program must behave, to reason about this behavior, and to be able to produce code from specifications in a semi-automatic fashion. We argue that a mild form of specification not only makes it possible to get programs running easier, but it also introduces students to a quite systematic way of approaching programming: reading and understanding specifications is seen as an unavoidable step in the programming process, as they are really the only place where the expected conduct of the system is described. By using formal techniques in these cases, where they are undoubtedly appropriate, we introduce formality without the need to resort to justifications with artificial or overly complicated examples.


Concurrent Programming Formal Specification Code Generation Safety Liveness Ada 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andrews, G.R., Schneider, F.B.: Concepts and notations for concurrent programming. In: Gehani, N., McGettrick, A.D. (eds.) Concurrent Programming, Addison-Wesley, Reading (1989)Google Scholar
  2. 2.
    Andrews, G.: Concurrent Programming: Principles and Practice. Benjamin/Cummings (1991)Google Scholar
  3. 3.
    Bruynooghe, M., Lau, K.-K. (eds.): Program Development in Computational Logic. LNCS, vol. 3049. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  4. 4.
    Burns, A., Wellings, A.: Concurrency in Ada. Cambridge University Press, Cambridge (1998)Google Scholar
  5. 5.
    Cohen, N.H.: Ada as a Second Language. McGraw-Hill, New York (1995)Google Scholar
  6. 6.
    Hanus, M., Kuchen, H., Moreno-Navarro, J.J., et al.: Curry: An integrated functional logic language. Technical report, RWTH Aachen (2000)Google Scholar
  7. 7.
    Feldman, M.B., Bachus, B.D.: Concurrent programming can be introduced into the lower-level undergraduate curriculum. In: Proceedings of the 2nd conference on Integrating technology into computer science education, pp. 77–79. ACM Press, New York (1997)CrossRefGoogle Scholar
  8. 8.
    Gehani, N.H.: Capsules: a shared memory access mechanism for Concurrent C/C++. IEEE Transactions on Parallel and Distributed Systems 4(7), 795–811 (1993)CrossRefGoogle Scholar
  9. 9.
    Hermenegildo, M., Bueno, F., Cabeza, D., Carro, M., García de la Banda, M., López García, P., Puebla, G.: The Ciao Multi-Dialect Compiler and System: An Experimentation Workbench for Future (C)LP Systems. In: Parallelism and Implementation of Logic and Constraint Logic Programming, April 1999, pp. 65–85. Nova Science, Commack (1999)Google Scholar
  10. 10.
    Herranz, A., Moreno, J.J.: On the design of an object-oriented formal notation. In: Fourth Workshop on Rigorous Object Oriented Methods, ROOM 4, March 2002, King’s College, London (2002)Google Scholar
  11. 11.
    William Higginbotham, C., Morelli, R.: A system for teaching concurrent programming. In: Proceedings of the twenty-second SIGCSE technical symposium on Computer science education, pp. 309–316. ACM Press, New York (1991)CrossRefGoogle Scholar
  12. 12.
    Hoare, C.A.R.: Monitors, an operating system structuring concept. Communications of the ACM 17(10), 549–557 (1974)zbMATHCrossRefGoogle Scholar
  13. 13.
    Jackson, D.: A Mini-Course on Concurrency. In: Twenty-second SIGCSE Technical Symposium on Computer Science Education, pp. 92–96. ACM Press, New York (1991)CrossRefGoogle Scholar
  14. 14.
    Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall, Upper Saddle River (1995)Google Scholar
  15. 15.
    Morales-Fernandez, R., Moreno-Navarro, J.J.: CC-Modula: A Modula-2 Tool to Teach Concurrent Programming. ACM SIGCSE Bulletin 21, 19–25 (1989)CrossRefGoogle Scholar
  16. 16.
    The Joint Task Force on Computing Curricula IEEE-CS/ACM. Computing Curricula (2001),
  17. 17.
    Persky, Y., Ben-Ari, M.: Re-engineering a concurrency simulator. In: Proceedings of the 6th annual conference on the teaching of computing and the 3rd annual conference on Integrating technology into computer science education, pp. 185–188. ACM Press, New York (1998)Google Scholar
  18. 18.
    Robbins, S.: Using remote logging for teaching concurrency. In: Procs. of the 34th SIGCSE Technical Symposium on Comp. Sci. Education, pp. 177–181. ACM Press, New York (2003)CrossRefGoogle Scholar
  19. 19.
    Taft, T.S., Duff, R.A., Brukardt, R.L., Ploedereder, E. (eds.): Consolidated Ada Reference Manual. Language and Standard Libraries International Standard ISO/IEC 8652/1995(E) with Technical Corrigendum 1. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  20. 20.
    van Lamsweerde, A.: Formal Specification: a Roadmap. In: Finkelstein, A. (ed.) The Future of Software Engineering, pp. 147–159. ACM Press, New York (2000)Google Scholar
  21. 21.
    Yeager, D.P.: Teaching concurrency in the programming languages course. In: Proceedings of the twenty-second SIGCSE technical symposium on Computer science education, pp. 155–161. ACM Press, New York (1991)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Manuel Carro
    • 1
  • Julio Mariño
    • 1
  • Ángel Herranz
    • 1
  • Juan José Moreno-Navarro
    • 1
  1. 1.Facultad de InformáticaUniversidad Politécnica de MadridBoadilla del Monte, MadridSPAIN

Personalised recommendations