Towards a formal approach

Reliability is the cornerstone of reuse. Hence, object-oriented implementation, design and analysis must first and foremost support the development of reliable software, should the original claim to promote the reuse of software ever come true. Validating software by means of testing alone is clearly insufficient. As argued in [Backhouse], the probability of finding an error is usually too small to view testing as a reliable method of detecting the error. The fallacy of any empirical approach to validating software, which includes quantitative measurements based on software metrics, is that in the end we just have to wait and see what happens. In other words, it is useless as a design methodology.

Formal specification -- contracts

type specification -- local properties
relational specification -- structural properties, type relations
functional specification -- requirements

Verification -- as a design methodology

reasoning about program specification/code

Runtime consistency -- invariance

behavioral types specify test cases
invariants and assertions monitor consistency

slide: Formal specification and verification

Verification should be at the heart of any design method. In addition to allowing us to reason about the specification and the code, the design process should result in an architectural description of the system as well as in a proof that the system meets its requirements. Looking at the various approaches to the specification and verification of software, we can see that the notion of invariance plays a crucial role in developing provably correct solutions for a variety of problems (cf. Gries, 1981; Backhouse, 1986; Apt and Olderog, 1991; Dahl, 1992). Invariance, as we observed when discussing object test methods, also play an important role in testing the runtime consistency of a system. Hence, from a pragmatic point of view, studying formal approaches may help us become aware of the properties that determine the runtime consistency of object-oriented systems. In part III (chapter 10), we will explore what formal methods we have available for developing object-oriented software. Our starting point will be the foundations underlying the notion of contracts as introduced in [Meyer88]. We will take a closer look at the relation between contracts and the specification of the properties of abstract data types. Also, we will look at methods allowing us to specify structural and functional relations between types, as may occur in behavioral compositions of objects. More specifically, we will study the means available to relate an abstract specification of the properties of a data type to a concrete implementation. These studies are based on an analysis of the notion of abstract data types, and the relation between inheritance and subtyping. In particular, we will look at rules to determine whether a subclass derived by inheritance conforms to the subtype relation that we may define in a formal approach to object types.

However, before we delve into the formal foundations of object-oriented modeling, we will first look at an example of application development and explore the design space of object-oriented languages and system implementation techniques. These insights will enable us to establish to what extent we may capture a design in formal terms, and what heuristics are available to accomplish the tasks remaining in object-oriented development.

[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

You may not copy or print any of this material without explicit permission of the author or the publisher. In case of other copyright issues, contact the author.