topical media & game development
Towards a formal approach
Reliability is the cornerstone of reuse.
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
As argued in [Backhouse]
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
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
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
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
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.
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.