Spine: Language for Pattern Verification

Abstract

Patterns are often described in terms of concrete examples in specific programming languages in catalogues (Gamma, Helm, Johnson, & Vlissides, 1995). The description is worded such that a practitioner in an object-oriented programming language will be able to understand the key points of the pattern and translate it into a programming language of their choice.This abstract description of patterns is well suited for intelligent readers, but less suited for automated tasks that must process pattern information. Furthermore, the way in which the pattern information is encoded is often strongly influenced by the type of processing that is being performed on the pattern. In this chapter, the Spine language will be presented as a way of representing Design patterns in a suitable manner for performing verification of a pattern’s implementation in a particular source language. It is used by a proof engine