Abstract
This paper is about formal development methods for concurrent programs. Interference is the bane of the quest for compositional methods for concurrency. Concepts from object-oriented languages are argued to be a promising way of taming interference. Two approaches to development are described which are applicable to differing degrees of interference.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
P. America, “Issues in the design of a parallel object-oriented language,” Formal Aspects of Computing, Vol. 1, No. 4, 1989.
P. America, “Formal techniques for parallel object-oriented languages,” in (Baeten and Groote, 1991), pp. 1–17, 1991.
P. America and J. Rutten, “A parallel object-oriented language: Design and semantic foundations,” PhD thesis, Free University of Amsterdam, 1989.
R.J.R. Back, “Refinement calculus, part II: Parallel and reactive systems,” in (de Bakker et al., 1990), pp. 67–93, 1989.
J.A. Bergstra and L.M.G. Feijs (Eds.), “Algebraic methods II: Theory tools and applications,” Vol. 490 of Lecture Notes in Computer Science, Springer-Verlag, 1991.
J.C.M. Baeten and J.F. Groote (Eds.), “CONCUR'91—Proceedings of the 2nd International Conference on concurrency theory,” Vol. 527 of Lecture Notes in Computer Science, Springer-Verlag, 1991.
L. Cardelli, J. Donahue, L. Glassman, M. Jordan, B. Kalsow, and G. Nelson, “Modula-3 report,” Technical Report 31, DEC Systems Research Center, Palo Alto, California, April 1988.
K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, 1988.
P. Collette, “Composition of assumption-commitment specifications in a UNITY style,” Science of Computer Programming, Vol. 23, pp. 107–126, 1994.
P. Collette, “Design of compositional proof systems based on assumption-commitment specifications—Application to UNITY,” PhD thesis, Louvain-la-Neuve, June 1994.
F.S. de Boer, “Reasoning about dynamically evolving process structure,” PhD thesis, Free University of Amsterdam, 1991.
J.W. de Bakker, W.-P. de Roever, and G. Rozenberg (Eds.), “Stepwise refinement of distributed systems,” Vol. 430 of Lecture Notes in Computer Science, Springer-Verlag, 1990.
C.C. de Figueiredo, “A proof system for a sequential object-based language,” PhD thesis, University of Manchester, August 1994.
J.V. Guttag and J.J. Horning, “Larch: Languages and tools for formal specification,” Texts and Monographs in Computer Science, Springer-Verlag, 1993, ISBN 0-387-94006-5/ISBN 3-540-94006-5.
M.-C. Gaudel and J.-P. Jouannaud (Eds.), “TAPSOFT'93: Theory and practice of software development,” Vol. 668 of Lecture Notes in Computer Science, Springer-Verlag, 1993.
C.A.R. Hoare, I.J. Hayes, He Jifeng, C.C. Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sørensen, J.M. Spivey, and B.A. Sufrin, “The laws of programming,” Communications of the ACM, Vol. 30, No. 8, pp. 672–687, 1987, see Corrigenda in Communications of the ACM, Vol. 30, No. 9, p. 770.
C.A.R. Hoare, “Recursive data structures,” International Journal of Computer & Information Sciences, Vol. 4, No. 2, pp. 105–132, 1975.
J. Hogg, “Islands: Aliasing protection in object-oriented languages,” in (Paepcke, 1991), 1991.
C.B. Jones, “Development methods for computer programs including a notion of interference,” PhD thesis, Oxford University, June 1981, Printed as: Programming Research Group, Technical Monograph 25.
C.B. Jones, “Specification and design of (parallel) programs,” in Proceedings of IFIP'83, North-Holland, 1983, pp. 321–332.
C.B. Jones, Systematic Software Development using VDM, Prentice-Hall International, second edition, 1990, ISBN 0-13-880733-7.
C.B. Jones, “Constraining interference in an object-based design method,” in (Gaudel and Jouannand, 1993), pp. 136–150, 1993.
C.B. Jones, “Reasoning about interference in an object-based design method,” in (Woodcock and Larsen, 1993), pp. 1–18, 1993.
W. Janssen, M. Poel, and J. Zwiers, “Action systems and action refinement in the development of parallel systems,” in (Baeten and Groote, 1991), pp. 298–316, 1991.
B.B. Kristensen, O.L. Madsen, B. Møller-Pedersen, and K. Nygaard, “Object oriented programming in the Beta programming language,” Technical Report, University of Oslo, September 1991.
K.R.M. Leino, “Toward reliable modular programs,” PhD thesis, California Institute of Technology, 1995.
C. Lengauer, “A methodology for programming with concurrency,” PhD thesis, Computer Systems Research Group, University of Toronto, 1982.
R.J. Lipton, “Reduction: A method of proving properties of parallel programs,” Communications of the ACM, Vol. 12, pp. 717–721, 1975.
B. Meyer, Object-Oriented Software Construction, Prentice-Hall, 1988.
R. Milner, J. Parrow, and D. Walker, “A calculus of mobile processes,” Information and Computation, Vol. 100, pp. 1–77, 1992.
E.-R. Olderog and K.R. Apt, “Using transformations to verify parallel programs,” in (Bergstra and Feijs, 1991), pp. 55–82, 1991.
A. Paepcke (Ed.), OOPSLA'91, ACM, ACM Press, November 1991.
A.W. Roscoe and C.A.R. Hoare, “Laws of occam programming,” Monograph PRG-53, Oxford University Computing Laboratory, Programming Research Group, February 1986.
K. Stølen, “Development of parallel programs on shared data-structures,” PhD thesis, Manchester University, 1990, available as UMCS-91-1-1.
K. Stølen, “A method for the development of totally correct shared-state parallel programs,” in (Baeten and Groote, 1991), pp. 510–525, 1991.
D. Walker, “Process calculus and parallel object-oriented programming languages,” in International Summer Institute on Parallel Computer Architectures, Languages, and Algorithms, Prague, 1993.
D. Walker, “Confluence of processes and systems of objects,” July 1995, CAAP'95.
J.C.P. Woodcock and P.G. Larsen (Eds.), “FME'93: Industrial-strength formal methods,” Vol. 670 of Lecture Notes in Computer Science, Springer-Verlag, 1993.
Q. Xu and J. He, “A theory of state-based parallel programming by refinement: Part I,” in J. Morris (Ed.), Proceedings of The Fourth BCS-FACS Refinement Workshop, Springer-Verlag, 1991.
Q. Xu, “A theory of State-based parallel programming,” PhD thesis, Oxford University, 1992.
A. Yonezawa (Ed.), ABCL: An Object-Oriented Concurrent System, MIT Press, 1990, ISBN 0-262-24029-7.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Jones, C.B. Accommodating interference in the formal design of concurrent object-based programs. Form Method Syst Des 8, 105–122 (1996). https://doi.org/10.1007/BF00122417
Issue Date:
DOI: https://doi.org/10.1007/BF00122417