Although nobody has so far showed how to formalize "design patterns", many of the design motifs that patterns contain can be formalized as demonstrated here for the "gang of four" patterns:
Tools can be used used to specify patterns and to verify that an implementation conforms with the specification:
I think there are 3 ways in which there could be a fruitful
interaction between ideas about patterns and about formal
or rigorous techniques (compare FormalMethods
- FormalTreatmentOfDesignPatterns. The patterns in e.g. GOF can be seen as functions: Problem --> Solution, and each piece of design can be seen as a composition: Solution*Solution*... By analysing them this way, we could hope to improve our understanding of how to document and apply patterns, possibly how to translate them into generic designs or language features and maybe how best to catalogue and search for them.
- PatternsOfModeling. Patterns can be applied to abstract models as well as end designs.
- PatternsOfRefinement?. This is a specialization of design patterns, in which you start with a formal model.
. I undertake to modify the above when and as
persuaded by any ensuing debate.
If you understand WhyPatternsAreDifferent
you might worry that any attempt to
formalize patterns lets people conveniently dodge
the integrative, generative, and human
aspects of patterns that contribute to the
QualityWithoutAName. That is, formal methods try to
give a name to the QualityWithoutAName, 'nuf said...
I'll advocate the formalization of patterns when society
believes it is a good idea to formalize poetry beyond
A rocket ship with 232 million dollars on the line, should not be reciting random poetry into the air out the exhaust pipe for a nice fireworks display. And, lately, are FormalistsTakingOverThisWiki?
I wholeheartedly agree with Jim that any attempt to formalize the notion of
patterns misses the boat, but I do think that there are things that can benefit
from formalization IN patterns.
Ward has noted elsewhere in WikiWikiWeb
that some of the coding patterns that
used to be used in assembly language coding have now been put into compilers. That sort
of growth from art to science over time will also take some of what's useful in certain
patterns and move them into tools and formal methods over time.
The point is not to formalize the "pattern" per se. The point is to formalize what the pattern
is referring to. Remember that the map is not the thing.
Kyle -- could you give an example of what you mean? For
example, when I look at http://csg.uwaterloo.ca/patterns.html
it doesn't strike any chords in me, and I think it is
counter to what we want to achieve. Alexander said:
I was no longer willing to start looking at any pattern unless
it presented itself to me as having the capacity to connect up
with some part of this quality [the quality without a name].
Unless a particular pattern actually was capable of generating
the kind of life and spirit that we are now discussing, and that
it had this quality itself, my tendency was to dismiss it, even
though we explored many, many patterns.
-- StephenGrabow?, "Christopher Alexander: The Search for
a new paradigm."
That URL just falls short on "life" and "spirit."
Eden A. H, J. Gil, A. Yehudai (1996). A Formal Language for Design Patterns. The 3rd Annual Conference on the Pattern Languages of Programs
- PLoP(Washington University technical report WUCS-97-07)
and Mikkonen,T., Formalizing Design Patterns, Proceedings of the International Conference on Software Engineering
, 1998. ACM Press. (p.115)
I agree with JimCoplien
's statement above. Formalizing
design patterns is too reminiscent of ToddCoram
's story under KoansMetaphorsAndParables
Don't get me wrong, I haven't got anything against the papers cited above
but I have encountered someone who's
never done any OOP (let alone used a pattern) who's decided to
define the meaning of "Design Pattern" mathematically. I'm not
making this up 8-(
^Insert extensions, remarks and pointers to news and list discussions.^
See also: PeopleInterestedInFormalPatterns
--- Reliable and timely
Dependable distributed system typically utilize a hierarchy of protocols to provide for reliable and timely services. Such protocols have both dependability and real-time attributes, and the analysis of these protocols is a problem of growing complexity.
The development of precise and accurate formal specifications of these protocols and their subsequent formal verification to gain assurance have been a great challenge. Exploiting the inherent modularity in the design of most dependable protocols, in this thesis, we present our modular approach to specification composition and verification of dependable distributed protocol. In particular, we consider redundancy management protocols that are needed to manage redundant resources used in the system for dependability purposes.
Utilizing building-block protocols inherently used in redundancy management protocols, we perform compositional specification and verification of a checkpointing and recovery protocol based on them.
The key idea is that if a library of these basic components, like the primitives and sub-protocols are being formulated, then these elements aid in systematic and hierarchical development of dependable distributed protocols.
The main contribution of this thesis to illustrate the fact that by defining a priori validated building-blocks for dependable distributed protocols, larger and more complex protocols can be easily specified and verified. For a mechanical support in formal verification process, we use formal tools such as Specware and PVS.