Reuse of verified design templates through extended pattern matching

CARE provides a framework for construction and verification of programs, based around the recording of reusable design knowledge in parameterized templates. This paper shows how pattern-matching can be used to aid in the selection and application of design templates from a reusable library. A general framework is presented which is independent of the particular matching algorithm used at the level of mathematical expressions. A prototype has been built which supports a large subset of the Z mathematical language