A Refinement Theory for Concurrent Object Oriented Languages
Resumo
A notion of refinement for concurrent object-oriented programs was originally presented in [3]. In this article we prove that the refinement relation associated to this notion is a congruence with respect to various standard programming language constructors, including parallel and sequential composition, conditionals, and non-deterministic internal choice. We also establish a weaker compositionality result for the atomic evaluation constructor, and illustrate how novel compositionality properties can be derived from the basic congruence property.
Palavras-chave:
Formal methods, Object oriented programming, Refinement, Concurrency
Referências
Paulo Borba. Semantics and Refinement for a Concurrent Object Oriented Language. PhD thesis, Oxford University, Computing Laboratory, Programming Research Group, July 1995.
Paulo Borba and Joseph Goguen. Ao operational semantics for FOOPS. In R. Wieringa and R. Feenstra, editors, Working papers ofthe International Workshop on Information Systems-Correctness and Reusability. September 1994.
Paulo Borba and Joseph Goguen. Refinement of concurrent object oriented programs. In Stephen Goldsack and Stuart Kent, editors, Formal Methods and Object Technology, Chapter 11. Springer-Verlag, 1996.
George Cleland and Donald MacKenzie. Inhibiting factors, market structure and the industrial uptake of formal methods. In International Workshop on Industrial Strength Formal Specification Techniques. IEEE Computer Society Press, Boca Raton, Florida, April 1995.
Joseph Goguen. Parameterized programming. Transactions on Software Engineering, SE-10(5) :528-543, September 1984.
Joseph Goguen and José Meseguer. Unifying functional, object-oriented and relational programming, with logical semantics. In Bruce Shriver and Peter Wegner, editors, Research Directions in Object-Oriented Programming, pages 417-477. MIT, 1987.
Cliff Jones. An object-based design method for concurrent programs. Technical Report UMCS-92-12-1, Department of Computer Science, University of Manchester, 1992.
Cliff Jones. Process-algebraic foundations for an object-based design notation. Technical Report UMCS-93-10-1, Department of Computer Science, University of Manchester, 1993.
Kevin Lano and Stephen Goldsack. Refinement and subtyping in formal object-oriented development. In R. Wieringa and R. Feenstra, editors, Working papers of the International Workshop on Information Systems-Correctness and Reusability. September 1994.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
Carroll Morgan. Programming from Specifications. Prentice Hall, second edition, 1994.
Gordon Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, September 1981.
David Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, 1986.
Paulo Borba and Joseph Goguen. Ao operational semantics for FOOPS. In R. Wieringa and R. Feenstra, editors, Working papers ofthe International Workshop on Information Systems-Correctness and Reusability. September 1994.
Paulo Borba and Joseph Goguen. Refinement of concurrent object oriented programs. In Stephen Goldsack and Stuart Kent, editors, Formal Methods and Object Technology, Chapter 11. Springer-Verlag, 1996.
George Cleland and Donald MacKenzie. Inhibiting factors, market structure and the industrial uptake of formal methods. In International Workshop on Industrial Strength Formal Specification Techniques. IEEE Computer Society Press, Boca Raton, Florida, April 1995.
Joseph Goguen. Parameterized programming. Transactions on Software Engineering, SE-10(5) :528-543, September 1984.
Joseph Goguen and José Meseguer. Unifying functional, object-oriented and relational programming, with logical semantics. In Bruce Shriver and Peter Wegner, editors, Research Directions in Object-Oriented Programming, pages 417-477. MIT, 1987.
Cliff Jones. An object-based design method for concurrent programs. Technical Report UMCS-92-12-1, Department of Computer Science, University of Manchester, 1992.
Cliff Jones. Process-algebraic foundations for an object-based design notation. Technical Report UMCS-93-10-1, Department of Computer Science, University of Manchester, 1993.
Kevin Lano and Stephen Goldsack. Refinement and subtyping in formal object-oriented development. In R. Wieringa and R. Feenstra, editors, Working papers of the International Workshop on Information Systems-Correctness and Reusability. September 1994.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
Carroll Morgan. Programming from Specifications. Prentice Hall, second edition, 1994.
Gordon Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, September 1981.
David Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, 1986.
Publicado
14/10/1996
Como Citar
BORBA, Paulo.
A Refinement Theory for Concurrent Object Oriented Languages. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 10. , 1996, São Carlos/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
1996
.
p. 39-55.
DOI: https://doi.org/10.5753/sbes.1996.24436.
