A formal template language enabling metaproof

Abstract

Design patterns are usually described in terms of instances. Templates describe sentences of some language with a particular form, generate sentences upon instantiation, and can be used to describe those commonly occurring structures that make a pattern. This paper presents FTL, a language to express templates, and an approach to proof with templates. This enables reuse at the level of formal modelling and verification: patterns of models are captured once and their structure is explored for proof, so that patterns instances can be generated mechanically and proved results related with the pattern can be reused in any context. The paper uses templates to capture the Z promotion pattern and metaproof to prove properties of Z promotion. The proved properties are applicable directly to Z promotions built by template instantiation. © Springer-Verlag Berlin Heidelberg 2006.