An introduction to TUG: a language for writing reusable formal program specifications

TUG (Tree Unified with Grammar) was developed to support a system to be developed through an integration of conventional software development, operational specification, rapid prototyping via software transformations, software reuse, and analysis of specifications and programs via testing and proofs. The language integrates various software development paradigms into a coherent whole to fit specific needs of developing organizations. This paper shows how to write reusable specifications in TUG. Compared to other existing specification languages, the advantages, disadvantages, limitations, and strengths of the language is discussed. The language improves the reusability of formal specifications in the following ways: (i) a developer can run a TUG specification as a prototype to study its behavior due to its executability at the front-end of the software life cycle, (ii) a developer can easily write a parametric program corresponding to its parametric specification due to the similar semantics.