Structuring Mechanisms for an Object-Oriented Formal Specification Language

  • Márcio Cornélio
  • Paulo Borba
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1844)


In this work we propose an extension of the MooZ formal specification language with support for parameterized packages. This enhances MooZ’s capabilities for software reuse and maintenance in the large. We discuss several design issues for MooZ’s structuring mechanisms: the distinction between inheritance and subtyping, values and objects, vertical and horizontal composition, packages and classes. We also analyse the impact of our design decisions on software reuse.


Formal Methods Object-Oriented Specification Parameterized Programming Language design 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alencar, A.J., Goguen, J.A.: OOZE: An Object Oriented Z Environment. In: ECOOP 1991 - V European Conference on Object-Oriented Programming, Geneva - Switzerland, Springer, Heidelberg (1991)Google Scholar
  2. 2.
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentide-Hall (1997)Google Scholar
  3. 3.
    Stroustrup, B.: The C++ Programming Language, 3rd edn. Addison-Wesley, Reading (1997)Google Scholar
  4. 4.
    de, V.A., Cordeiro, O.: From MooZ to Eiffel: A Rigorous Approach to System Development. Master’s thesis, Universidade Federal de Pernambuco, Departmento de Informática (1994) (in Portuguese)Google Scholar
  5. 5.
    Watt, D.A.: Programming Languages Concepts and Paradigms. C. A. R. Hoare Series Editor. Prentice Hall International, Englewood Cliffs (1989)Google Scholar
  6. 6.
    Aranha, D., Borba, P.: Parameterized packages and Java. In: II Brazilian Symposium on Programming Languages, Campinas, Brazil, pp. 208–218 (September 1997)Google Scholar
  7. 7.
    Batory, D., Singhal, V., et al.: The GenVoca Model of Software-System Generators. IEEE Software, 89–94 (September 1994)Google Scholar
  8. 8.
    Motta, G.H.M.B.: Object-Oriented Formal Specifications: Application in the Development of an Effort Eletrocardiogram Processing System. Master’s thesis, Departamento de Informática, Universidade Federal de Pernambuco (1992) (in Portuguese)Google Scholar
  9. 9.
    Goguen, J.: Reusing and interconnecting software components. Computer 19(2), 16–28 (1986)CrossRefGoogle Scholar
  10. 10.
    Goguen, J.: Principles of parameterized programming. In: Biggerstaff, T., Perlis, A. (eds.) Software Reusability. Concepts and Models, ch. 7, vol. I, pp. 159–225. ACM Press, New York (1989)Google Scholar
  11. 11.
    Goguen, J., Socorro, A.: Module composition and system design for the object paradigm. Journal of Object-Oriented Programming 7(9) (1995)Google Scholar
  12. 12.
    Goguen, J., Winkler, T.: Introducing OBJ3. Technical Report SRI-CSL-88- 9, SRI International, Computer Science Lab. In: Meseguer, J., Futatsugi, K., Jouannaud, J.-P. (eds.) Applications of Algebraic Specification Using OBJ (August 1988) Revised version to appear with additional authors edited by Joseph GoguenGoogle Scholar
  13. 13.
    Spivey, J.M.: Understanding Z: A specification language and its formal semantics. Cambridge University Press, Cambridge (1988)zbMATHGoogle Scholar
  14. 14.
    Spivey, J.M.: The Z Notation: a reference manual, Hoare, C.A. Series (ed.) 2nd edn. Prentice Hall International, Englewood Cliffs (1992)Google Scholar
  15. 15.
    Woodcock, J., Davies, J.: Using Z - Specification, Refinement and Proof. C. A. R. Hoare Series Editor. Prentice-Hall International, Englewood Cliffs (1996)zbMATHGoogle Scholar
  16. 16.
    Guttag, J.V., Horning, J.J., Modet, A.: Report on the Larch Shared Language - Version 2.3. Technical report, Digital Equipment Corporation, SRC Research Report 58 (1990)Google Scholar
  17. 17.
    Arnold, K., Gosling, J.: The Java Programming Language. Addison-Wesley, Reading (1996)zbMATHGoogle Scholar
  18. 18.
    Cardelli, L., Wegner, P.: On understanding types, data abstraction and polymorphism. Computing Surveys 17(4) (December 1985)Google Scholar
  19. 19.
    Cornélio, M.L.: Design and evaluation of an object-oriented formal specification language. Master’s thesis, Universidade Federal de Pernambuco, Departamento de Informática, Recife - PE (1998)Google Scholar
  20. 20.
    de, P.D., Machado, L.: EASY — An Environment for Simulation of Artificial Neural Networks. Master’s thesis, Departamento de Informática, Universidade Federal de Peranambuco (1994) (in Portuguese)Google Scholar
  21. 21.
    Borges, R., Ierusalimschy, R.: Módulosem Linguages Orientadas a Objetos. In: I Brazilian Symposium on Programming Languages, Belo Horizonte, Brazil, pp. 371–384 (September 1996)Google Scholar
  22. 22.
    Duke, R., King, P., Rose, G.A., Smith, G.: The Object-Z Specification Language: Version 1. Technical Report 91-1, Department of Computer Science, University of Queensland, Software Verification Center (April 1991)Google Scholar
  23. 23.
    Meira, S.L., Cavalcanti, A.L.C.: MooZ Case Studies. In: Stepney, S., Barden, R., Cooper, D. (eds.) Object Orientation in Z, Workshops in Computing. ch. 5, pp. 37–58. Springer, Heidelberg (1992)Google Scholar
  24. 24.
    Meira, S.R.L., Cavalcanti, A.L.C.: The MooZ Specification Language. Technical report, Universidade Federal de Pernambuco, Departamento de Informática, Recife - PE (1992), Also available at
  25. 25.
    Garland, S.J., Guttag, J.V., Horning, J.J.: An Overviewo f Larch. In: Lauer, P.E. (ed.) Functional Programming, Concurrency, Simulation and Automated Reasoning. LNCS, vol. 693, pp. 329–348. Springer, Heidelberg (1993)Google Scholar
  26. 26.
    Ogden, W.F., Sitaraman, M., et al.: Special Feature: Component-Based Software Using RESOLVE. Software Engineering Notes 19(4), 21–67 (1994)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Márcio Cornélio
    • 1
  • Paulo Borba
    • 1
  1. 1.Centro de InformáticaUniversidade Federal de PernambucoRecifeBrasil

Personalised recommendations