Abstract
An object-oriented approach to program specification and verification was developed by Ole-Johan Dahl with the long-term Abel project. Essential here was the idea of reasoning about an object in terms of its observable behavior, where the specification of an object’s present behavior is given by means of its past interactions with the environment. In this paper, we review some of the ideas behind this approach and show how they can be fruitfully extended for reasoning about black-box components in open object-oriented distributed systems.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)
Agha, G.A., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. Journal of Functional Programming 7(1), 1–72 (1997)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4), 181–185 (1985)
Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Systems. Texts and Monographs in Computer Science. Springer, Berlin (1991)
Blair, L., Blair, G.: Composition in multi-paradigm specification techniques. In: Ciancarini, R., Fantechi, A., Gorrieri, R. (eds.) Proc. 3rd International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 1999), pp. 401–418. Kluwer Academic Publishers, Dordrecht (1999)
Boiten, E., Derrick, J., Bowman, H., Steen, M.: Constructive consistency checking for partial specification in Z. Science of Computer Programming 35(1), 29–75 (1999)
Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading (1999)
Broy, M., Stølen, K.: Specification and Development of Interactive Systems. Monographs in Computer Science. Springer, Heidelberg (2001)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)
Dahl, O.-J.: Can program proving be made practical? In: Amirchahy, M., Néel, D. (eds.) Les Fondements de la Programmation. Institut de Recherche d’Informatique et d’Automatique, Toulouse, France, pp. 57–114 (December 1977)
Dahl, O.-J.: Object-oriented specification. In: Shriver, B., Wegner, P. (eds.) Research Directions in Object-Oriented Programming. Series in Computer Systems, pp. 561–576. The MIT Press, Cambridge (1987)
Dahl, O.-J.: Verifiable Programming. International Series in Computer Science. Prentice Hall, New York (1992)
Dahl, O.-J.: The roots of object orientation: the Simula language. In: Broy, M., Denert, E. (eds.) Software Pioneers: Contributions to Software Engineering. Springer, Heidelberg (2002)
Dahl, O.-J., Nygaard, K.: SIMULA, an ALGOL-based simulation language. Communications of the ACM 9(9), 671–678 (1966)
Dahl, O.-J., Myhrhaug, B., Nygaard, K.: (Simula 67) Common Base Language. Technical Report S-2, Norsk Regnesentral (Norwegian Computing Center), Oslo, Norway (May 1968)
Dahl, O.-J., Owe, O.: Formal development with ABEL. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 320–362. Springer, Heidelberg (1991)
Dahl, O.-J., Owe, O.: Formal methods and the RM-ODP. Research Report 261, Department of informatics, University of Oslo, Norway (May 1998)
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 47. Cambridge University Press, New York (1998)
Derrick, J., Bowman, H., Steen, M.: Viewpoints and objects. In: Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1995. LNCS, vol. 967, pp. 449–468. Springer, Heidelberg (1995)
Fischer, C.: CSP-OZ: a combination of Object-Z and CSP. In: Bowman, H., Derrick, J. (eds.) Proc. 2nd IFIP Workshop on Formal Methods for Open Object- Based Distributed Systems (FMOODS), pp. 423–438. Chapman and Hall, London (1997)
Ghezzi, C., Jazayeri, M.: Programming Language Concepts, 3rd edn. John Wiley & Sons, Chichester (1998)
Goguen, J., Tardo, J.: An introduction to OBJ: A language for writing and testing formal algebraic program specifications. In: Gehani, N., McGettrick, A. (eds.) Software Specification Techniques. Addison-Wesley, Reading (1986)
Guttag, J.V., Horning, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)
Hoare, C.A.R.: An Axiomatic Basis of Computer Programming. Communications of the ACM 12, 576–580 (1969)
Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1985)
International Telecommunication Union. Open Distributed Processing — Reference Model parts 1–4. Technical report, ISO/IEC, Geneva (July 1995)
Jacobs, B.: Inheritance and cofree constructions. In: Cointe, P. (ed.) ECOOP 1996. LNCS, vol. 1098, pp. 210–231. Springer, Heidelberg (1996)
Johnsen, E.B., Owe, O.: Composition and refinement for partial object specifications. In: Proc. 16th International Parallel & Distributed Processing Symposium (IPDPS 2002), Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA 2002). IEEE Computer Society Press, Los Alamitos (2002)
Johnsen, E.B., Owe, O.: A compositional formalism for object viewpoints. In: Jacobs, B., Rensink, A. (eds.) Proc. 5th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2002), pp. 45–60. Kluwer Academic Publishers, Dordrecht (2002)
Johnsen, E.B., Owe, O., Munthe-Kaas, E., Vain, J.: Incremental fault-tolerant design in an object-oriented setting. In: Proc. Asian Pacific Conference on Quality Software (APAQS 2001), pp. 223–230. IEEE Computer Society Press, Los Alamitos (2001)
Johnsen, E.B., Zhang, W., Owe, O., Aredo, D.B.: Combining graphical and formal development of open distributed systems. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 319–338. Springer, Heidelberg (2002)
Jones, C.B.: Development Methods for Computer Programmes Including a Notion of Interference. PhD thesis, Oxford University, UK (June l981)
Kahn, G.: The semantics of a simple language for parallel programming. In: Rosenfeld, J.L. (ed.) Information Processing 1974: Proc. IFIP Congress 1974, pp. 471–475. IFIP, North-Holland Publishing Co., Amsterdam (1974)
Kiczales, G., Lamping, J., Menhdhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997)
Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems 16(6), 1811–1841 (1994)
Malabarba, S., Pandey, R., Gragg, J., Barr, E., Barnes, J.F.: Runtime support for type-safe dynamic Java classes. In: Bertino, E. (ed.) ECOOP 2000. LNCS, vol. 1850, pp. 337–361. Springer, Heidelberg (2000)
Matsuoka, S., Yonezawa, A.: Analysis of inheritance anomaly in object-oriented concurrent programming languages. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 107–150. The MIT Press, Cambridge (1993)
Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Transactions on Software Engineering 7(4), 417–426 (1981)
Nierstrasz, O.: A survey of object-oriented concepts. In: Kim, W., Lochovsky, F. (eds.) Object-Oriented Concepts, Databases and Applications, pp. 3–21. ACM Press and Addison-Wesley (1989)
Nygaard, K., Dahl, O.-J.: Simula 67. In: Wexelblat, R.W. (ed.) History of Programming Languages. ACM Press, New York (1981)
Owe, O.: Partial logics reconsidered: A conservative approach. Formal Aspects of Computing 5, 208–223 (1993)
Owe, O., Ryl, I.: A notation for combining formal reasoning, object orientation and openness. Research Report 278, Department of informatics, University of Oslo, Norway (November 1999)
Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Communications of the ACM 15(12), 1053–1058 (1972)
Parnas, D.L., Wang, Y.: The trace assertion method of module interface specification. Technical Report 89-261, Department of Computing and Information Science, Queen’s University at Kingston, Kingston, Ontario, Canada (October 1989)
Smith, G.: The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)
Smith, S.F., Talcott, C.: Modular reasoning for actor specification diagrams. In: Ciancarini, R., Fantechi, A., Gorrieri, R. (eds.) Proc. 3rd International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 1999), pp. 401–418. Kluwer Academic Publishers, Dordrecht (1999)
Soundarajan, N., Fridella, S.: Inheritance: From code reuse to reasoning reuse. In: Devanbu, P., Poulin, J. (eds.) Proc. Fifth International Conference on Software Reuse (ICSR5), pp. 206–215. IEEE Computer Society Press, Los Alamitos (1998)
Walker, D.: Objects in the π-calculus. Information and Computation 116(2), 253–271 (1995)
Wang, A.: Generalized types in high-level programming languages. Research Report in Informatics 1, Institute of Mathematics, University of Oslo, Cand. Real thesis (January 1974)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Johnsen, E.B., Owe, O. (2004). Object-Oriented Specification and Open Distributed Systems. In: Owe, O., Krogdahl, S., Lyche, T. (eds) From Object-Orientation to Formal Methods. Lecture Notes in Computer Science, vol 2635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39993-3_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-39993-3_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21366-6
Online ISBN: 978-3-540-39993-3
eBook Packages: Springer Book Archive