This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Logical Theory of Interfaces and Objects
June 2002 (vol. 28 no. 6)
pp. 548-575

Abstract—This paper motivates and describes a logic-based approach to specifying and reasoning about interfaces and objects that focuses on separation of concerns issues. The approach is based on the Abstract Design View (ADV), a software design model for object-oriented systems. The model was originally introduced to characterize, in an informal and practical setting, a clear separation between objects, which we called Abstract Design Objects (ADOs) and their interfaces (ADVs). The objects capture the basic concern (the fundamental computation algorithm and basic functionality as it is relevant to an application domain), while the interfaces capture special concerns such as user interface, control, timing, and distribution. First, we analyze the ADV design model in order to precisely characterize the interfaces, their associated objects, and the relationship between them. This relationship, which we call “views-a,” is formally characterized through its semantic properties. Then, we present one possible approach to formalizing interfaces, objects, and the “views-a” relationship. The central mathematical tools used for this purpose are temporal logic and some tools from category theory. The formal approach is illustrated by examples that show how the interface and related objects and the views-a relationship can be used in object-oriented specifications. Once the designer identifies the concerns, the theory provides a formal means to define, separate, and use interfaces to capture the specific concerns in object-oriented design. Further, the theory provides a formal means to combine the interfaces that capture the concerns. We also show how the theory enables the designer to perform relevant analysis activities while modeling with separation of concerns in mind. The theory can be used to derive dynamic and structural properties of the interface objects and the views-a relationship. In particular, we can use the theory to derive global properties of interfaces that capture special concerns from the local properties of their related objects.

[1] WATCOM$\big. VX\!\cdot\! REXX\bigr.$for OS/2 Programmer's Guide and Reference. Waterloo, Ontario, Canada, 1993.
[2] M. Abadi and L. Cardelli, “An Imperative Object Calculus,” Proc. Sixth Int'l Joint Conf. Theory and Practice of Software Development (TAPSOFT '95), 1995.
[3] P.S.C. Alencar, D.D. Cowan, T. Kuntz, and C.J.P. Lucena, “A Formal Architectural Design Patterns-Based Approach to Software Understanding,” Proc. Fourth Workshop Program Comprehension (WPC '96), ICSE-18, Mar. 1996.
[4] P.S.C. Alencar, D.D. Cowan, and C.J.P. Lucena, “The Formalization of Architectural Design Patterns,” Proc. Formal Methods Europe (FME '96) Symp. Industrial Benefits and Advances in Formal Methods, Mar. 1996.
[5] P.S.C. Alencar, D.D. Cowan, C.J.P. Lucena, and L.C.M. Nova, “Formal Specification of Reusable Interface Objects,” Proc. Symp. Software Reusability (SSR '95), pp. 88–96, 1995.
[6] H. Barringer, “The Use of Temporal Logic in the Compositional Specification of Concurrent Systems,” Temporal Logic and Their Applications, A. Galton, ed., 1987.
[7] T. Bolognesi and E. Brinkma, “Introduction to the ISO Specification Language LOTOS,” The Formal Description Technique LOTOS, P.H.J.V. Eijk, C.A. Vissers, and M. Diaz, eds., pp. 23–73, 1989.
[8] G. Booch, Object Oriented Design with Applications, Benjamin/Cummings Publishing Company, Inc., Redwood City, Calif., 1991.
[9] R.H. Bourdeau and B.H.C. Cheng, “A Formal Semantics of Object Models,” IEEE Trans. Software Eng., vol. 21, pp. 799–821, Oct. 1995.
[10] F. Civello, “Roles for Composite Objects in Object-Oriented Analysis and Design,” Proc. Eighth Ann. Conf. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'93), pp. 376-393, 1993.
[11] S. Conrad, M. Gogolla, and R. Herzig, “TROLL Light: A Core Language for Specifying Objects,” Technical Report 92-02, Dept. of Computer Science, Technische Univ. Braunschweig, Braunschweig, 1992.
[12] S. Cook and J. Daniels, Designing Object Systems: Object-Oriented Modelling with Syntropy, Prentice Hall, New York, 1994.
[13] W.R. Cook and J.A. Palsberg, “A Denotational Semantics of Inheritance and Its Correctness,” Proc. Ann. ACM Conf. Object-Oriented Programming Systems, Languages and Applications (OOPSLA '89), pp. 433–443, 1989.
[14] D.D. Cowan et al., “Program Design Using Abstract Data Views—An Illustrative Example,” Technical Report 92-54, Computer Science Dept., Univ. of Waterloo, Ontario, Canada, Dec. 1992.
[15] D.D. Cowan, R. Ierusalimschy, C.J.P. Lucena, and T.M. Stepien, “Abstract Data Views,” Structured Programming, vol. 14, no. 1, pp. 1–13, Jan. 1993.
[16] D.D. Cowan, R. Ierusalimschy, C.J.P. Lucena, and T.M. Stepien, “Application Integration: Constructing Composite Applications from Interactive Components,” Software Practice and Experience, vol. 23, no. 3, pp. 255–276, Mar. 1993.
[17] D.D. Cowan and C.J.P. Lucena, “Abstract Data Views: An Interface Specification Concept to Enhance Design,” IEEE Trans. Software Eng., vol. 21, no. 3, pp. 229–243, Mar. 1995.
[18] D.D. Cowan, C.J.P. Lucena, and R.G. Veitch, “Towards CAAI: Computer Assisted Application Integration,” Technical Report 93-17, Computer Science Dept. and Computer Systems Group, Univ. of Waterloo, Ontario, Canada, Jan. 1993.
[19] R. Duke, P. King, and G. Smith, “Formalising Behavioural Compatibility for Reactive Object-Oriented Systems,” Proc. 14th Australian Computer Science Conference (ACSC '91), 1991.
[20] E. Durr and E. Dusink, “The Role of VDM++ in the Development of a Real-Time Tracking and Tracing System,” Proc. Formal Methods Europe (FME '95), pp. 64–72, 1993.
[21] M. Ehrig and B. Mahr, Fundamentals of Algebraic Specification 1. Berlin: Springer-Verlag, 1985.
[22] E. Emerson, "Temporal and Modal Logic," Handbook of Theoretical Computer Science, J. Leeuwen, ed., chapter 16, pp. 995-1, 072. Elsevier, 1990.
[23] J. Fiadeiro and T. Maibaum, Describing, Structuring, and Implementing Objects. Springer-Verlag, 1991.
[24] J. Fiadeiro and T. Maibaum, “Temporal Theories as Modularization Units for Concurrent System Specification,” Formal Aspects of Computing, vol. 4, no. 4, 1992.
[25] J.L. Fiadeiro and T.S.E. Maibaum, “Sometimes `Tomorrow' is `Sometime,'” Temporal Logic; Lecture Notes in Artificial Intelligence, vol. 827, pp. 48–66, 1994.
[26] J.L. Fiadeiro and T.S.E. Maibaum, “Design Structures for Object-Based Systems,” technical report, Dept. of Computing, Imperial College of Science and Technology, London, 1995.
[27] E. Gamma et al., Design Patterns: Elements of Object-Oriented Software, Addison-Wesley, Reading, Mass., 1994.
[28] J. Goguen, “Sheaf Semantics for Concurrent Interacting Objects,” Math. Structures in Computer Science, vol. 11, pp. 159–191, 1992.
[29] J.A. Goguen, "Reusing and Interconnecting Software Components," Computer, Feb. 1986.
[30] J.V. Guttag, J.J. Horning, K.D. Jones, S.J. Garland, A. Modet, and J. Wing, “Larch: Languages and Tools for Formal Specification,” Texts and Monographs in Computer Science, 1993.
[31] W. Hursch and C.V. Lopes, “Separation of Concerns,” Technical Report NU-CCS-95-3, Computer Science Dept., Northeastern Univ., Boston, 1995.
[32] H.M. Jarvinen, R. Kurki-Suonio, M. Sakkinen, and K. Systa, “Object-Oriented Specification of Reactive Systems,” Proc. 12th Int'l Conf. Software Eng., pp. 63–71, 1990.
[33] C.B. Jones, “An Object-Based Design Method for Concurrent Programs,” Technical Report UMCS-92-12-1, Computer Science Dept., Manchester Univ., U.K., 1992.
[34] S. Kent and K. Lano, “Axiomatic Semantics for Concurrent Object-Oriented Systems,” Technical Report AFRODITE AFRO/IC/SKKL/SEM/VI, Dept. of Computing, Imperial College of Science and Technology, London, 1994.
[35] B.B. Kristensen, “Object-Oriented Modeling with Roles,” Theory and Practice of Object-Oriented Systems, issue on subject-oriented programming, 1995.
[36] K. Lano, Formal Object-Oriented Development. 1995.
[37] K. Lano, “Reactive System Specification and Refinement,” Proc. Sixth Int'l Joint Conf. Theory and Practice of Software Development (TAPSOFT '95), 1995.
[38] K. Lano, “The Semantics of Real-time Action Logic,” Technical Report COFM-2517-3, Dept. of Computing, Imperial College of Science and Technology, London, 1996.
[39] C.J.P. Lucena, D.D. Cowan, and A.B. Potengy, “A Programming Model for User Interface Compositions,” Anais do V Simpósio Brasileiro de Computação Gráfica e Processamento de Imagens, (SIBGRAPI '92), Nov. 1992.
[40] G. Malcolm, “Interconnections of Object Specifications,” Proc. BCS FACS Workshop Formal Methods and Object-Orientation, 1995.
[41] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
[42] I. Maung, “Behavioral Subtyping and Substitutability,” Proc. BCS FACS Workshop Formal Methods and Object-Orientation, 1995.
[43] H.A. Partsch, Specification and Transformation of Programs. Springer-Verlag, 1990.
[44] A.B. Potengy, C.J.P. Lucena, and D.D. Cowan, “A Programming Approach for Parallel Rendering Applications,” Technical Report 93-62, Computer Science Dept. and Computer Systems Group, Univ. of Waterloo, Ontario, Canada, Mar. 1993.
[45] W. Pree, Design Patterns for Object-Oriented Software Development, Addison-Wesley, Reading, Mass., 1994.
[46] R.S. Pressman, Software Engineering—A Practitioner's Approach, 3rd ed., McGraw-Hill, New York, 1992.
[47] C.L. Chang, R.A. Stachowitz, and J.B. Combs, “Validation of Nonmonotonic Knowledge-Based Systems,” Proc. IEEE Int'l Conf. Tools for Artificial Intelligence, Nov. 1990.
[48] C. Seguin and V. Wiels, “Using a Logical and Categorical Approach for the Validation of Fault-Tolerant Systems,” Proc. Formal Methods Europe (FME '96) Symp. Industrial Benefits and Advances in Formal Methods, pp. 347–366, Mar. 1996.
[49] G. Smith, “A Logic for Object-Z,” Technical Report 94-48, Dept. of Computer Science, Univ. of Queesland, Australia, 1994.
[50] M. Snoeck and G. Dedene, “Existence Dependency: The Key to Semantic Integrity between Structural and Behavioral Aspects of Object Types,” IEEE Trans. Software Eng., vol. 24, no. 4, pp. 233-251, 1998.
[51] E.Y. Wang, H.A. Richter, and B.H.C. Cheng, “Formalizing and Integrating the Dynamic Model within OMT,” Proc. 19th Int'l Conf. Software Eng., pp. 45–55, May 1997.
[52] G. Wiederhold, P. Wegner, and S. Ceri, “Towards Megaprogramming,” Comm. ACM, vol. 35, no. 11, Nov. 1992.
[53] R.J. Wieringa, W. De Jonge, and P. Spruit, “Using Dynamic Classes and Role Classes to Model Object Migration,” Theory and Practice of Object Systems, vol. 1, no. 1, pp. 61–83, 1995.
[54] R.J. Wieringa, R. Jungclaus, P. Hartel, and G. Saake, “OMTroll—Object Modeling in Troll,” Proc. Int'l Workshop Information Systems—Correctness and Reusability, pp. 267–283, 1993.
[55] M. Wirsing, “Algebraic Specification,” Handbook of Theoretical Computer Science, vol. B, pp. 675-788, Amsterdam: North Holland, 1990.

Index Terms:
Abstract design views, objects, specification, verification, user interfaces, logic, concurrency.
Citation:
Paulo S.C. Alencar, Donald D. Cowan, Carlos J.P. Lucena, "A Logical Theory of Interfaces and Objects," IEEE Transactions on Software Engineering, vol. 28, no. 6, pp. 548-575, June 2002, doi:10.1109/TSE.2002.1010059
Usage of this product signifies your acceptance of the Terms of Use.