Sciweavers

Share
FM
2006
Springer

A Formal Template Language Enabling Metaproof

10 years 5 months ago
A Formal Template Language Enabling Metaproof
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.
Nuno Amálio, Susan Stepney, Fiona Polack
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FM
Authors Nuno Amálio, Susan Stepney, Fiona Polack
Comments (0)
books