Edinburgh Research Explorer

Automatic verification of Java design patterns

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publicationAutomated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages4
ISBN (Print)0-7695-1426-X
Publication statusPublished - 2001


Design patterns are widely used by object oriented designers and developers for building complex systems in object oriented programming languages such as Java. However, systems evolve over time, increasing the chance that the pattern in its original form will be broken. We attempt to show that many design patterns (implemented in Java) can be verified automatically. Patterns are defined in terms of variants, mini-patterns, and artifacts in a pattern description language called SPINE. These specifications are then processed by Hedgehog, an automated proof tool that attempts to prove that Java source code meets these specifications.

    Research areas

  • Java, automatic programming, object-oriented programming, program verification, specification languages, theorem proving, Hedgehog, Java design patterns, Java source code, SPINE, automated proof tool, automatic verification, complex systems, mini-patterns, object oriented designers, object oriented programming languages, pattern description language, specifications, Books, Bridges, Buildings, Computer languages, Formal languages, Informatics, Memory management, Production facilities, Runtime

ID: 11477799