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

Software has traditionally been designed using one of two basic divide-and-conquer paradigms: decomposition by form or decomposition by function. Decomposition by form implies dividing an object into smaller objects, and decomposition by function implies dividing an action into a number of actions. We believe that both paradigms are needed in the software design process as is also the case in classical engineering design. Decomposition by form is currently supported by object-oriented design methods such as those proposed by Booch [Boo91] or Rumbaugh [R+91], while decomposition by function is supported by Structured Design as described by Yourdon and others [WM85, YC79]. The approach proposed by Rumbaugh supports both form and function, but they are treated distinctly. We have proposed a unified design method that incorporates both decomposition by form and decomposition by function.

Our design approach constructs software system designs using composition operators and two types of component specifications: application components and interface components. The application components are Abstract Data Types (ADTs) and are the same as those defined by Hoare [Hoa72] and others. The interface components called Abstract Data Views (ADVs) [CILS93a, CILS93b], 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 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 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 [CL93, HHG90].

The composition operators constitute a formally defined set of specification constructors that operate on ADVs and ADTs to produce composite ADVs or ADTs from simpler components, or sets or sequences of simpler components. The constructors defined by our design method support decomposition by function, while decomposition by form is supported by the fact that both the instantiations of ADTs and ADVs are objects. The semantics of these constructors and ADVs have been chosen to encourage reuse of design specifications through separation of concerns. The composition operations are guarded composition by inclusion and composition through inheritance. Guarded composition by inclusion implies reuse of syntactic components, whereas composition by inheritance implies modification of the component syntax. Composition by inclusion is guarded to enforce constraints on what information a component type is able to access from its composite type; everything a component type must know about the composite type is provided through parameters at instantiation.

Software designs must also express other types of relationships or constraints among the components. For example, the many-to many relationships that arise in entity-relationship designs for databases. Rumbaugh's design approach allows expression of these types of relationships. Relationships among the component ADTs in our approach can be expressed by specializing an ADT with the addition of an invariant or by the use of an invariant in an ADV component, since invariants provide a powerful mechanism for expressing constraints. For example, the fact that an arc in a graph must be terminated by two nodes can be expressed in an invariant.

BothADTsandADVs can be specified using textual and graphical formalisms, and a mapping exists between the two forms of expression. The current textual formalism is based on object-oriented versions of VDM[Jon90] and VDM++ [Dur93] (an extension that handles concurrency). The present graphical formalism called ADVcharts [CCL94, CCL93] is used for designing user interfaces, and is based on state-machine approaches similar to Statecharts[Har87] and Objectcharts[CHB92]. We have created a graphical formalism because visualizing the design is easier, and sequential and time relationships are more readily apparent. Both the textual and graphical representations support the specification of structure and behaviour. Structure of designs is provided by the composition operators, while behaviour is expressed through either temporal logic or state machine formalisms.

We have chosen formal methods as the basis for our approach to design specification because they support unambiguous specification, allow for tool-supportedmathematical reasoning about these specifications and could allow rapid prototypingof functionality. Formal methods and reuse are closely related; reusing a component developed using formal methods spreads the higher development costs over more projects while improving both the quality of the development process and resulting software systems.

ADVs have been used to support user interfaces for games and a graph editor [C+92], to interconnect modules in a user interface design system (UIDS) [LCP92], to support concurrency in a cooperative drawing tool, to implement a ray-tracer in a distributed environment [PLC93], and to produce a scientific visualization system. A research prototype of the VX?REXX [VRe93] system was motivated by the idea of composing applications in the ADV/ADT style. ADVcharts have been tested by using them to produce several different software designs and to redesign and reengineer the Rita text editor, an existing interactive software system [CMPS91, Smi94, CCCLS94]. In addition, we have shown in [CILS93b] and [CLV93] how ADVs can be used to compose complex applications from simpler ones in a style which is similar to some approaches to megaprogramming [WWC92].

Many papers referenced in this proposal are available via anonymous ftp from [csg.uwaterloo.ca] at the University of Waterloo. The names of the papers are in the file ?pub/ADV/README? and the papers are in the directories ?pub/ADV/demo?, ?pub/ADV/theory?, and ?pub/ADV/tools?.

2 Formal Methods

We have devised a set of specification constructors (described in the background section) to build complex ADTs and ADVs from simpler ADTs and ADVs. Designs using the ADV/ADT approach and these constructors can be expressed in an extended version of VDM or using ADVcharts. We need to continue the development of a formal semantics for both these modes of expression.

We have recently defined a formal semantics for the specification constructors. Using these semantics we can show that applying a constructor to a complex ADT or ADV only augments its previous properties. In this context, we have proven a modularization theorem that shows that a composition of ADTs obtained through a sequence of applications of the constructors to these ADTs is equivalent to the composition of the ADVs related to these ADTs when the constructors are applied in the same order. The proof of the modularization theorem about reuse through ADVs was obtained by using a semantics for the constructors given in terms of textual substitution in a manner similar to that used by Hoare [Hoa72]. A more precise statement of the proposed modularization theorem follows: an ADT specification extended by other reusable ADT specifications through the use of a given set of specification constructors can be interpreted (or viewed) as an equivalent ADV specification provided that the original ADT can be interpreted (or viewed) by an associated ADV that is extended by the application of the same given set of specification constructors applied to the ADVs associated with the reused ADTs (see Figure 1). Using the terminology adopted in [TM87], we can say that we have a ?modularization theorem? for the reuse-in-the-large of ADTs interpreted as ADVs.

E - Extension of by means of reusable

ADTs using specification constructors

ADTSADTE - Extension of by means of reusable

ADVs associated with ADTs using

specification constructors

ADVSADVI - Interpretation of in terms ofSADVSADT'''I - Interpretation of in terms ofSADVSADTS - ADT SpecificationADTS - ADV SpecificationADVEADTIADT,ADVEADVSADT'SADV'SADVSADTIADT,ADV'

Figure 1: The Modularization Theorem for Reuse of ADTs interpreted through ADVs

The dynamic properties of ADVs can be expressed using a temporal logic formalism. Using this formalism we are able to talk about instances of ADVs and ADTs and analyze consistency between an ADV and an associated ADT (vertical consistency) and between several ADVs associated with the same ADT (horizontal consistency). These results on reuse and consistency have been reported in [ACCCL94].

Although we have achieved these results, our formalization does not allow us to reason about the properties of designs. Since ADTs and ADVs can be understood in terms of mathematical theories and ADVs view or interpret ADTs, we plan to use ?interpretation between theories? [End72] expressed in logic in order to produce an integrated theory of ADTs and ADVs with accompanying inference rules.

Similarly the ADVchart graphical formalism has been interpreted in terms of statecharts (one form of operational semantics). An operational semantics approach does not provide the ability to reason about the interactive properties of human interfaces. Since statecharts have been successfully formalized before in terms of denotational semantics [HRR92], we also plan to use denotational semantics accompanied by inference rules to express the formalism represented by ADVcharts.
Using these formal bases for ADVs we will gain the advantages mentioned previously and also should be able to reason about interactive systems and interface designs as suggested in [MP90, ND90].

3 A Preliminary Logical Theory of ADVs

We have described a preliminary (non-logical) semantics for the ADV design concept which supports reuse-in-thelarge. The semantics for ADVs were given in terms of textual substitution in the same style used by Hoare in [Hoa72]. In this context, the semantics of all the specification constructors used in the theory were presented. We have also presented a modularization theorem for reuse of ADTs interpreted through ADVs.

The notation in which the semantics is expressed in this preliminary version of the theory was chosen for its readability thus providing a clear understanding of the intuitive aspects of the concepts. In a next step we will go further by capturing the semantics in logic by using interpretation between theories. This kind of formalization which was also used in [TM87] proved very useful in the formulation of a similar modularization theorem (in their case, related to program reification), and will allow us to reason about reusable designs. Let us now indicate how this style of logical formalization can be used as a formal basis for the ADV approach.

According to the adopted logical approach we identify 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 logic that can be used for supporting object-oriented specifications. This is done because the logical approach advocates that the process of program development consists of the manipulation of specification theories but, in practice and as usual, it is much easier to manipulate presentations of theories in which just the (non-logical) axioms of the theory are presented. Particularly, the approach to be used is a proof-theoretic one based on a combination of temporal logic and category theory following[FM92, FM93] that was initially developed with the purpose of formalising modularization techniques for reactive systems. We will adopt a temporal logic with a (global) discrete linear time structure that is fairly close to those used [Pnueli 77; Barringer 87; Manna, Pnueli 90; Manna, Pnueli 91], thus allowing easier assessment of the support for modular specification that will be described. We will also use the fact that temporal logics may be defined that satisfy, to some extent, institution (Burstall, Goguen 84) and, hence, that temporal theories may be used as modularization units for concurrent system specification. We emphasize here that the logics that can be used for supporting object-oriented specification are somewhat more complex than a pure temporal logic, and involves deontic notions as well as action modalities besides temporal operators [Fiadeiro, Maibaum 90: Fiadeiro et al. 90]. However, the structuring mechanisms are independent of the underlying logic and, hence, it is simpler to formalise objects as structuring units for concurrent systems specification based on a simpler logic than using all the logical machinery that is more appropriate for object description. Neverthless, there are many similarities between the full logical apparatus and the one based only on temporal logic and therefore we can think about temporal logic specification units as objects in the object-oriented sense.

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.

As a first step, following the "institutional way", we have to introduce the notions of object signature and, for each signature, interpretation structure, language and satisfaction (truth) relation between interpretation structures and formulae. We have to describe the temporal fragment of the language and present the notion of locality (data

abstraction, encapsulation of a set of attributes). Furthermore, we have to show what is an object description (that will be formed by an object signature and a set of formulas which are the axioms of the description). We also have to describe how to reason about local descriptions of ADVs and ADTs, i.e. how to reason about the properties of a particular object description.

As a second step, we have to show how we can put descriptions together in order to form the description of more complex objects. In other words, we want to give a logical formal semantics for the ADV specification constructors for composition, inheritance, sets and sequences. We shall see that the adopted logical formalism not only deeply characterizes the difference between the specification constructors as, for instance, the difference between composition and inheritance, but also allows us to characterize the specification constructors in a more detailed way (e.g., it will be possible to differentiate between inheritance and particularization). In the first step we have to define the syntax and semantics of one adopted logic, and show how a (primitive) system component could be described as a theory presentation. Then, we have to show how such descriptions can be put together in order to provide the specification of systems of interconnected components, and how concurrency is supported. In this context, we have to define a category of object descriptions that is finitely cocomplete and we have to show how the interaction between objects can be expressed through diagrams. We have also to show how to use the diagrams to describe the joint behavior of objects taking into account their interaction.

Having developed a collection of theories that act as descriptions of objects, we can use these theories to describe a more complex system by assembling as nodes of a diagram as many instances of these theories as required, and by using morphisms between these theories as edges of the diagram in order to establish the required interconnections. If the category is ?well behaved? (i.e. finitely cocomplete) such a diagram may be collapsed to another theory that provides the description of the complex system as an object itself, and that can then be used in order to derive properties of the global system, or as a node in another diagram, i.e. as a component of another system. Hence, we have to provide a notion of morphism between theory presentations and prove that the resulting category allows for such colimits to be computed.

The morphisms between theory presentations define the notion of structure that the actual formalism provides for specification. As structure-preserving mappings, morphisms establish the relationship that must exist between two object descriptions so that one of them may be considered as a component of the other. Intuitively, this corresponds to the notion of interpretation between theories. When we use the notion of institution, this relationship consists of a translation between the languages of the two descriptions (a signature morphism) such that the theorems of one of them are translated to theorems of the second one. That is, we take the preservation of theorems (the meaning of a theory presentation) as the criterion for considering that a theory presentation describes a component of a system described through another theory presentation. It is also possible to restrict the properties that we actually want to preserve along a morphism, namely only safety or liveness properties, leading to different notions of structure. Actually, when we adopt the pure temporal logic formalism, we require the preservation of both safety and liveness properties. In this context, results such as the modularization theorem for reuse of ADT s interpreted through ADV s can be established.

Finally, we show how we can obtain the joint behavior of the interconnection of many individualobject descriptions of ADVs and ADTs through the adopted specification constructors and how the concurrent aspects of the resulting descriptions can be treated. The joint behavior can be given in terms of the colimit in the category of object descriptions of the diagram involving the individual descriptions. We should notice here that theories act as "types" in the sense that several instances of the same theory may be used in the same diagram to express the fact that there are several components of the system that are of the same "type" (follow the same behavior). We shall see how we can distinguish between these various instances. In other words, a theory act as a "generic" object. We also have to show how to derive global properties, i.e. properties of the society of objects. In fact, being an object description, the description of the joint behavior of the individual descriptions has its own properties besides the properties of each individual object description. In particular, an ADV object description has its own properties besides the properties of its associated ADT and its components ADVs.

It is worthy to note that it is up to the specifier to interpret the absence of conservation along certain morphisms. For example, the lack of conservation with respect to liveness properties along some individual description morphisms should not worry the specifier because these descriptions may be intended to be passive objects and, hence, the

satisfaction of liveness requirements is not necessary. Other kinds of analysis that can be performed at this level concern the detection of deadlock situations that result from the lack of conservation with respect to safety properties.

4 Related Topics

Tools and Notation: We expect one result of our research into ADVs to be a software environment to support cooperative design and implementation using the ADV/ADT approach. The various components of the environment will be based on the underlying theory that our research group is currently investigating. It is still premature to produce an entire environment, but we are investigating tools and notations that we know will be useful in this environment. The current theory of ADVs has concentrated on the use of ADVs as user interfaces, and the supporting textual and graphical notations have been directed toward that goal. Investigations reported in [CL93] indicate that ADVs can be used to characterize interfaces between other media and ADTs, and between ADTs. We are investigating modifications to the notations in order to express these new relationships.

Design Tools: The current textual and graphical formalisms associated with the Abstract Data View model are manipulated manually. Computer-based tools are required if we expect designers to use these formalisms to support the design activity. Specialized systems to draw and annotate ADVcharts, transform ADVcharts into equivalent textual formalisms, animate designs, and check consistency properties are essential tools.

We also intend to develop tools based on the theory described earlier in this proposal to assist the designer in reasoning about properties of interactive system designs such as invariance, response and precedence [MP90, ND90]. Working on these design tools is going on related to the use of the Talisman software engineering environment.

Implementation Tools: The Abstract Data View design model can be realized using many different software implementation strategies. We intend to examine and categorize these different strategies and produce tools, both for direct implementation and to assist with the transformation of designs into programs. For example, the VX?REXX programming system [VRe93], which was originally developed as a prototype in our research group, is almost a direct implementation of the Abstract Data View model for one specific programming environment. VX?REXX allows the designer/programmer to translate a design directly into an operating program, thus simplifying many of the steps in the software development cycle. Other programming environments are being examined to determine if it is practical to implement similar strategies.

Design Methods ? Case Studies: The value of a software design model, such as the Abstract Data View Model, should be measured in terms of its ability to handle the design of significant software systems. In this regard, we have already performed a number of software design and implementation case studies. We intend to continue further case studies in which we will design new applications and also redesign and reengineer existing software systems. For example, we will investigate the redesign of the Gemini electronic mail package [CS92], the user interfaces to the JANET [CFGS88] class of local area networks, and the design of an editor to support cooperative work on linear graphs. We expect to use many of the case studies as the base for a design approach based on Abstract Data Views.

There are a number of software architectures, particularly in the area of user interfaces, which emphasize separation of concerns, that is, placing specific functions within designated modules or objects. Although these architectures describe the separation of concerns, they generally do not present a method of achieving this separation. Because the Abstract Data View Model and its accompanying formalisms both isolate the user interaction modes from the application and support composition, we believe they provide a method which will direct the designer to designs that maintain the separation of concerns. One case study [Smi94, CCCLS94] that has been completed, supports this view. We will continue to investigate this support of separation through the design case studies. Studying the separation of concerns using this model should lead to a more formal approach for identifying and classifying reusable components.

We also are going to investigate how existing design methods such as Structured Analysis [DeM78, PM84, You89] and Design [WM85, YC79], JSD [Jac83], Object-Oriented Analysis[CY91] and Design [Boo91, WBWW90], and

Rumbaugh [R+91] can be used in conjunction with the ADV/ADT approach. All these methods have brought some rigour to the process of creating, and maintaining software systems for a broad variety of applications. We intend to extend the rigour of these and other methods by developing a system that helps the designer formally document steps in whichever design method is being used. Such a system should provide a formal basis for many of the reification methods that are needed to produce an implementation from a design specification.

References

[ACCCL94] P.S.C. Alencar, L.M.F. Carneiro-Coffin, D. D. Cowan, and C.J.P. Lucena. The Semantics of Abstract Data Views: A Design Concept to Support Reuse-in-the-Large. In Proceedings of the Colloquium on Object-Orientation in Databases and Software Engineering (to appear), May 1994.

[Boo91] Grady Booch. Object Oriented Design with Applications. The Benjamin/Cummings Publishing Company, Inc., 1991.

[C+92] D. D. Cowan et al. Program Design Using Abstract Data Views?An Illustrative Example. Technical Report 92?54, Computer Science Department, University of Waterloo, Waterloo, Ontario, Canada, December 1992.

[CCCLS94] L.M.F. Carneiro-Coffin, D. D. Cowan, C.J.P. Lucena, and D. Smith. An Experience Using JASMINUM ? Formalization Assisting with the Design of User Interfaces. In Proceedings of the Workshop on Research Issues between Software Engineering and Human-Computer Interaction (to appear), Sorrento, May 1994.

[CCL93] L. M. F. Carneiro, D. D. Cowan, and C. J. P. Lucena. ADVcharts: a Visual Formalism for Interactive Systems - position paper. In SIGCHI Bulletin, pages 74?77, 1993.

[CCL94] L. M. F. Carneiro, D. D. Cowan, and C. J. P. Lucena. ADVcharts: a Visual Formalism for Interactive Systems. In Proceedings of the York Workshop on Formal Methods for Interactive Systems (to appear). Springer, 1994.

[CFGS88] D. D. Cowan, S. L. Fenton, J. W. Graham, and T. M. Stepien. Networks for Education at the University of Waterloo. Computer Networks and ISDN Systems, 15:313?327, 1988.

[CHB92] D. Coleman, F. Hayes, and S. Bear. Introducing Objectcharts or How to Use Statecharts in ObjectOriented Design. IEEE Transactions on Software Engineering, 18(1), 1992 1992.

[CILS93a] D. D. Cowan, R. Ierusalimschy, C. J. P. Lucena, and T. M. Stepien. Abstract Data Views. Structured Programming, 14(1):1?13, January 1993.

[CILS93b] 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, 23(3):255? 276, March 1993.

[CL93] D. D. Cowan and C. J. P. Lucena. Abstract Data Views: A Module Interconnection Concept to Enhance Design for Reusability. Technical Report 93?52, Computer Science Department and Computer Systems Group, University of Waterloo, Waterloo, Ontario, Canada, November 1993.

[CLV93] D. D. Cowan, C. J. P. Lucena, and R. G. Veitch. Towards CAAI: Computer Assisted Application Integration. Technical Report 93?17, Computer Science Department and Computer Systems Group, University of Waterloo, Waterloo, Ontario, Canada, January 1993.

[CMPS91] D. D. Cowan, E. W. Mackie, G. M. Pianosi, and G. de V. Smit. Rita - An Editor and User Interface for Manipulating Structured Documents. Electronic Publishing, Origination, Dissemination and Design, 4(3):125?150, September 1991.

[CS92] D. D. Cowan and T. M. Stepien. Electronic Communication and Distance Education. In Supplementary Proceedings of the Fourth International Conference on Computers and Learning, pages 14?16, 1992.

[CY91] P. Coad and E. Yourdon. Object-Oriented Analysis. Yourdon Press, Prentice-Hall, 1991.

[DeM78] T. DeMarco. Structured Analysis and System Specification. Yourdon Press, 1978.

[Dur93] E. H. Durr. VDM++ Language Reference Manual. Afrodite Project Partners, afro/cg/ed/lrm/vs edition, July 1993.

[End72] H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, New York, 1972.

[FM92] J. Fiadeiro and T. Maibaum. Temporal Theories as Modularization Units for Concurrent System Specification. Formal Aspects of Computing, 4(4), 1992.

[FM93] J. Fiadeiro and T. Maibaum. Verifying for Reuse: Foundations of Object-oriented System Verification. Technical report, Imperial College of Science and Technology, University of London, London, 1993.

[Har87] D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8:231?274, 1987.

[HHG90] Richard Helm, Ian M. Holland, and Dipayan Gangopadhyay. Contracts: Specifying Behavioral Compositions in Object-Oriented Systems. In OOPSLA'90, pages 169?180, 1990.

[Hoa72] C. Hoare. Proof of Correctness of Data Representations. Acta Informatica, 1(4):271?281, 1972.

[HRR92] J.J.M. Hooman, M. Ramesh, and W.P.de Roever. A Compositional Axiomatization of Statecharts. Theoretical Computer Science, 101:289?335, 1992.

[Jac83] M. A. Jackson. System Development. Computer Science. Prentice-Hall, 1983.

[Jon90] C. B. Jones. Systematic Software Development Using VDM. Prentice-Hall, second edition, 1990.

[LCP92] C. J. P. Lucena, D. D. Cowan, and A. B. Potengy. A Programming Model for User Interface Compositions. In Anais do V Simp?osio Brasileiro de Computac??ao Gr?afica e Processamento de Imagens, SIBGRAPI'92, Aguas de Lind?oia, SP, Brazil, November 1992.

[MP90] Z. Manna and A. Pnueli. Tools and Rules for the Practicing Verifier. Technical Report STAN-CS-90- 1321, Stanford University, July 1990.

[ND90] K.T. Narayana and S. Dharap. Invariant Properties in a Dialog System. In Proceedings of the ACM SIGSOFT International Workshop on Formal Methods in Software Development, May 1990.

[PLC93] A. B. Potengy, C. J. P. Lucena, and D. D. Cowan. A Programming Approach for Parallel Rendering Applications. Technical Report 93?62, Computer Science Department and Computer Systems Group, University of Waterloo, Waterloo, Ontario, Canada, March 1993.

[PM84] J. Palmer and S. McMenamin. Essential Systems Analysis. Yourdon Press, Prentice-Hall, 1984.

[R+91] James Rumbaugh et al. Object-Oriented Modeling and Design. Prentice Hall, 1991.

[Smi94] D. Smith. Abstract Data Views: A Case Study Evaluation. Technical Report 94?19, University of Waterloo, Computer Science Department, Waterloo, Ontario, April 1994.

[TM87] W. M. Turski and T. S. E. Maibaum. The Specification of Computer Programs. Addison-Wesley, 1987.

[VRe93] WATCOM VX?REXX for OS/2 Programmer's Guide and Reference. Waterloo, Ontario, Canada, 1993.

[WBWW90] R. Wirfs-Brock, B. Wilkerson, and L. Wiener. Designing Object-Oriented Software. Prentice-Hall, 1990.

[WM85] P. T. Ward and S. J. Mellor. Structured Development for Real-Time Systems. Yourdon Press, PrenticeHall, 1985.

[WWC92] G. Wiederhold, P. Wegner, and S. Ceri. Towards Megaprogramming. CACM, 35(11), November 1992.

[YC79] E. Yourdon and L. Constantine. Structured Design. Prentice-Hall, 1979.

[You89] E. Yourdon. Modern Structured Analysis. Prentice-Hall, 1989.