page 1  (9 pages)
2to next section

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.