Towards a Logical Theory of ADVs

P. S. C. Alencar ? L. M. F. Carneiro-Coffin y D.D. Cowan z C.J.P. Lucena x

Abstract

In this position paper we motivate and describe a preliminary logical theory for Abstract Data Views. Abstract Data Views (ADVs) define interfaces between application components or between application components and an "external" environment such as a user or a network. Abstract Data Views (ADVs) are Abstract Data Types (ADTs) that have been augmented with event-driven input and output operations and a mapping that ensures an ADV interface conforms to the state of its associated ADT. Different ADVs may view the same ADT since interfaces can support alternate "views" of data, providing the design satisfies certain consistency obligations. In order to maintain separation of concerns and promote design reuse, ADTs are specified to have no knowledge of their associated ADVs. ADVs can be seen as a way of providing language support for the specification and abstraction of inter-object behavior. The adopted logical approach identifies the individual formal units (objects) that compose the specification of a system with theories, i.e., ADVs and ADTs are represented through theories in a temporal logic with a (global) discrete linear time structure that can be used for supporting object-oriented specifications. Essentially, according to the adopted logical formalism, signatures are used (structures of non-logical language) as a means of localizing change by a logical role in the formalization of encapsulation. This enables local reasoning to be performed over components of a system. Furthermore, the adoption of an open semantics requires that objects are not taken in isolation but are open to interference from the environment, a requisite for compositionality and, finally, morphisms are used as a means of recording the component structure of an object, i.e., a formalization of the component-of relationship and of the other ADV specification constructors. In fact, a calculus of object-based systems must describe these specification constructors in logic and use them as a structuring mechanism for verification.

1 Motivation

This paper addresses the question: ?How do we build practical software (object-oriented) design systems based on formal methods, and how do we make them accessible and usable for the designer and implementor?? We have already created a software design model, called the Abstract Data View (ADV), which models the interfaces to a highly interactive software system and emphasizes the separation of concerns between the interface and the application component. We believe that this ADV model can be used to specify the functionality or interfaces to other system components as well as user interfaces.

Our research focuses on software design methods, tools, support structures and software implementation strategies in which reuse of design components and the ability to represent formally most steps in the design process are of fundamental importance. Formal methods have been chosen because they allow unambiguous specification and tool-supported mathematical reasoning about specifications.

?P. S. C. Alencar is a Visiting Professor in the Computer Science Department at the University of Waterloo, Waterloo, Ontario, Canada and is currently on leave from the Departamento de Ci?encia da Computac??ao, Universidade de Bras??lia, Bras??lia, Brazil. Email: alencar@csg.uwaterloo.ca yL. M. F. Carneiro-Coffin is a PhD candidate in the Computer Science Department at University of Waterloo and holds a doctoral fellowship from CAPES (the Brazilian Research Council). Email: lmfcarne@neumann.uwaterloo.ca
zD. D. Cowan is a Professor in the Computer Science Department at the University of Waterloo, Waterloo, Ontario, Canada. Email: dcowan@csg.uwaterloo.ca
xC.J.P. Lucena is a Visiting Professor in the Computer Science Department at the University of Waterloo, Waterloo, Ontario, Canada and is currently on leave from the Departamento de Inform?atica, Pontif??cia Universidade Cat?olica do Rio de Janeiro, Brazil. Email: lucena@csg.uwaterloo.ca