Design Verification Patterns - Formal Methods and Hybrid Real-Time Systems - page 400

The idea is rather natural, and one may wonder why it has not been done
already. Here it helps to look at history: In the 1990ies, software was coded
using languages like c , and systematic designs were very hard to discover in
the programs that resulted from this activity. Components were statements,
and analysis would be at a similar low level; it would focus on programming
language semantics and the corresponding program correctness theories as for
instance consolidated in Hoare and He's ”Unified Theory of Programming” [11].
Since then, the demand for more software to increasingly ecient computers
that find applications in the most diverse areas - ubiquitous computing - means
that the level of abstraction is lifted. There is increased use of object oriented
languages and design notations like UML [25,7], beginning experiments with
reuse of components [28], and concern for architecture [1]. These ideas are com-
bined with formal techniques and gains increasing popularity through efforts of
Meyer [19], which are continued in tool developments like JML [3].
Thus, modern software relies on datatypes and common functions as embod-
ied in the standard class libraries of objected oriented programming languages.
A corresponding level of structuring constructs comes with the practical use of
design patterns [15,6]. They may be the ”PID”s for the practicing software en-
gineer, but what are their properties, and how may these properties be used to
analyze applications?
A Design Verification Pattern. As an introduction to properties of design
patterns, we may look at the ancestor to all design patterns: The procedure
pattern . A (side-effect free) procedure p has an input or value parameter x and
computes an output or result y :
p ( value x ; result y )
With axiomatic semantics, we know that it may be fully specified in terms of
two predicates, a pre- and a post-condition: p.pre ( x )and p.post ( x , y ), where
the pre-condition specifies the domain of the procedure, and the post-condition
specifies the effect in the form of an input-output relation.
Analysing Properties. It is also clear that an implementer of p has an oblig-
ation to guarantee the post-condition, but only when one can rely on the pre-
condition. This is the basis for verifying correctness of the component p .From
our point of view, it is also the design verification pattern . The lemmas that can
be used in an application. Just before a call p ( e, r ), the application must assert
that the the procedure can relay on the pre-condition with e for x , p.pre [ e/x ].
Then, after the call, it is legitimate to assume the post-condition with a similar
substitution, p.post [ e/x , r/y ], and use it in an analysis of application properties.
Much research in verification has focused on the obligations of the implemen-
tors. We are less concerned with this, because with increasing reuse, components
are developed by specialists - the PhDs, who should be able to deal with the
task. In contrast, the components are used in many contexts, so the lemmas for-
mulated in the assert and assume conditions are a higher level start for verifying