J.O. Hallstrom and N. Soundarajan (USA)
Design patterns, software specifications, formal methods.
Design patterns are valuable both for designing and for
documenting software systems. Patterns are usually de
scribed informally. While informal descriptions are cer
tainly useful, in order to be sure that designers have a pre
cise understanding of the requirements that must be met
when applying a given pattern, and to be able to reliably
predict the behaviors that systems built using specific pat
terns will exhibit, we also need precise specifications of the
patterns. In this paper, we apply an approach to formally
specifying patterns  to the Memento pattern as a case
study. One important aspect of patterns is their flexibility.
Our case study shows that this flexibility is not compro
mised by our formalization. Indeed, the case study shows
that for some patterns, the formalization reveals increased
opportunities for variation.