A Functional Implementation of the Formal Template Language

Abstract

There has been growing interest in using the Z notation to describe design patterns and to encourage model driven development, but these are often expressed in terms of instances, rather than in a more general form. Instead of relying on the interpretation of instances, the Formal Template Language (FTL) has been used with Z as a means of capturing patterns in a framework that generates code on instantiation, thereby allowing reuse at the level of modelling and verification in a formal way. Until now, the instantiation of these templates has been manual. We present an implementation of the FTL in Haskell that allows the automatic generation of sentences from templates and evaluation environments. Our implementation uses Haskell and Happy (a functional parser generator for Haskell) to generate a parser that performs semantic analysis on given templates within specific environments to produce instantiations. By construction our implementation is faithful to the FTL specification in Z, by exploiting the commonalities between this specification and Haskell itself.