Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Formalising Design Patterns

    1st BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 23rd - 24th September 1996


    K. Lano, J.C. Bicarregui & S. Goldsack


    This paper views design patterns [5] as a transformation from a "before" system consisting of a set of classes (often a single unstructured class) into an "after" system consisting of a collection of classes organised by the pattern.

    To prove that these transformations are formal refinements, we adopt a version of the Object Calculus [4] as a semantic framework. We make explicit the conditions under which these transformations are formally correct.

    We give some additional design pattern transformations which have been termed "annealing" in the VDM++ world, which include the introduction of concurrent execution into an initially sequential system.

    We show that these design patterns can be classified on the basis of a small set of fundamental transformations which are reflected in the techniques used in the proof of their correctness.


    PDF filePDF Version of this Paper (198kb)