Abstract
We extend the action system formalism with a notion of objects that can be dynamically created, active and distributed. With this extension we can model class-based systems as action systems. Moreover, as the introduced constructs can be translated into ordinary action systems, we can use the theory developed for action systems, especially the refinement calculus, even for class-based systems. We show how inheritance can be modelled in different ways via class refinement. Refining a class with an other class within the refinement calculus ensures that the original behavior of the class is maintained throughout the refinements. Finally, we show how to reuse refinements and entire class modules in a refinement step.
Preview
Unable to display preview. Download preview PDF.
References
P. America, J.W. de Bakker, J.N. Kok, and J.J.M.M. Rutten. Operational semantics of a parallel object-oriented language. In Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages, pages 194–208, 1986.
P. America, J.W. de Bakker, J.N. Kok, and J.J.M.M. Rutten. Denotational semantics of a parallel object-oriented language. Information and Computation, 83(2):152–205, 1989.
J.-R. Abrial. The B-Book. Cambridge University Press, 1996.
G. Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, 1986.
M. Abadi and K.R.M. Leino. A logic of object-oriented programs. In Theory and Practice of Software Development, TAPSOFT'97, volume 1214 of Lecture Notes in Computer Science, Springer-Verlag, 1997.
R.-J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications. Volume 131 of Mathematical Centre Tracts. Mathematical Centre, Amsterdam, 1980.
R.J.R. Back. Procedural abstraction in the refinement calculus. Technical Report, åbo Akademi University, Department of Computer Science, Turku, Finland 1987.
R.J.R. Back. Refinement calculus, part II: parallel and reactive programs. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 67–93, Springer-Verlag, 1990.
R.J.R. Back, M. Büchi, and E. Sekerinski. Action-based concurrence and synchronization for objects. In Proceedings of the 4th AMAST Workshop on Real-Time Systems, Concurrent, and Distributed Software, Ciutad de Mallorca, Springer-Verlag, 1997.
C. Bailes and R. Duke. The Ecology of class refinement. In J.M. Morris and C. Shaw, editors, Proceedings of the 4th Refinement Workshop, January 1991, Cambridge, UK. Workshops in Computing, pp. 185–196, Springer Verlag.
R.J.R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. Distributed Computing, 3(2):73–87, 1983.
M.M. Bonsangue and J.N. Kok. The weakest precondition calculus: recursion and duality. Formal Aspects of Computing, 6A:788–800, 1994.
M.H. Brown and M.A. Najork. Distributed active objects. SRC Research Report 141a, DEC Palo Alto CA, 1996.
R.J.R. Back and K. Sere. Superposition refinement of parallel algorithms. In Parker, K.R. and Rose, editors, Proceedings of the IFIP Working Conference on Formal Description Techniques-IV, pages 475–494. North-Holland Publishing Company, 1992.
R.J.R. Back and K. Sere. Action systems with synchronous communication. In E.-R. Olderog, editor, Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi, IFIP Transactions A-56, pages 107–126, North-Holland Publishing Company, 1994.
R.J.R. Back and K. Sere. From action systems to modular systems. Software — Concepts and Tools, 17, Springer Verlag, 1996.
L. Cardelli. A language with distributed scope. Computing Systems 8(1):27–29, 1995.
K.M.Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.
C. Hewitt. Viewing control structures as patterns of passing messages. Artificial Intelligence 8(3), 1977.
U. Hensel, M. Huisman, B. Jacobs, and H. Tews. Reasoning about classes in object-oriented languages: logical models and tools. To appear in Proceedings of ESOP/ETAPS 1998, Lecture Notes in Computer Science, Springer-Verlag, 1998.
C.A.R. Hoare. Proofs of correctness of data representation. Acta Informatica, 1(4):271–281, 1972.
H.-M. Järvinen and R. Kurki-Suonio. DisCo specification language: marriage of actions and objects. In Proceedings of the 11th International Conference on Distributed Computing Systems, IEEE Computer Society Press, pages 142–151, 1991.
C.B. Jones. A π-calculus semantics for an object-based design notation. In Proceedings of CONCUR'93, volume 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993.
L. Lamport. The temporal logic of actions. Research report 79, DEC Systems research Center, 1991. To appear in ACM Transactions on Programming Languages and Systems.
K. Lano and H. Haughton. Reasoning and refinement in object-oriented specification languages. In European Conference on Object-Oriented Programming'92, volume 615 of Lecture Notes in Computer Science, Springer-Verlag 1992.
A. Mikhajlova and E. Sekerinski. Class refinement and interface refinement in object-oriented programs. In Proceedings of the Fourth International Formal Methods Europe Symposium (FME'97), volume 1313 of Lecture Notes in Computer Science, Springer-Verlag, 1997.
C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems 10:3, pages 403–419, 1988.
J.M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287–306, 1987.
D.A. Naumann. Predicate transformer semantics of an Oberon-like language. In E.-R. Olderog, editor, Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi, IFIP Transactions A-56, North-Holland Publishing Company, 1994.
B. Strulo. How firing conditions help inheritance. In J.P. Bowen and M.G. Hinchey, editors, ZUM'95: The Z Formal Specification Notation, volume 967 of Lecture Notes in Computer Science, Springer-Verlag 1995.
K. Sere and M. Waldén. Data refinement of remote procedures. In M. Abadi and T. Ito, editors, Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS'97), Sendai, Japan, volume 1281 of Lecture Notes in Computer Science, pages 267–294, Springer-Verlag, 1997.
R.T. Udink and J.N. Kok. ImpUNITY: UNITY with Procedures and Local Variables. In Proceedings of Mathematics of Program Construction '95, volume 947 of Lecture Notes in Computer Science. Springer-Verlag, 1995.
D.J. Walker. Objects in the π-calculus. Information and Computation, 116(2):253–271, 1995.
M. Waldén. Layering distributed algorithms. Technical report No 121, Turku Centre for Computer Science, Turku, Finland, 1997. To appear in Proceedings of the 2nd B conference, France, April 1998.
J. von Wright. The lattice of data refinement. Acta Informatica, 31(2):105–135, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonsangue, M.M., Kok, J.N., Sere, K. (1998). An approach to object-orientation in action systems. In: Jeuring, J. (eds) Mathematics of Program Construction. MPC 1998. Lecture Notes in Computer Science, vol 1422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054286
Download citation
DOI: https://doi.org/10.1007/BFb0054286
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64591-7
Online ISBN: 978-3-540-69345-1
eBook Packages: Springer Book Archive