Teaching How to Derive Correct Concurrent Programs from State-Based Specifications and Code Patterns
- 273 Downloads
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.
KeywordsConcurrent Programming Formal Specification Code Generation Safety Liveness Ada
Unable to display preview. Download preview PDF.
- 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.Andrews, G.: Concurrent Programming: Principles and Practice. Benjamin/Cummings (1991)Google Scholar
- 4.Burns, A., Wellings, A.: Concurrency in Ada. Cambridge University Press, Cambridge (1998)Google Scholar
- 5.Cohen, N.H.: Ada as a Second Language. McGraw-Hill, New York (1995)Google Scholar
- 6.Hanus, M., Kuchen, H., Moreno-Navarro, J.J., et al.: Curry: An integrated functional logic language. Technical report, RWTH Aachen (2000)Google Scholar
- 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.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
- 14.Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall, Upper Saddle River (1995)Google Scholar
- 16.The Joint Task Force on Computing Curricula IEEE-CS/ACM. Computing Curricula (2001), http://www.computer.org/education/cc2001/
- 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
- 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