Semantics-based tools for a specification-support environment

Abstract

We describe recently developed semantics-based support tools for Z, a mathematical specification language based on typed set theory. Z has proven very useful and popular with a number of industrial as well as academic software developers. These tools are components of Forsite, a support environment currently under development to integrate languages and operations with formally defined semantics and implementable operations. We anticipate that these tools will impose a de facto standard for the language. Z has undergone a noteworthy chronology of development and use. It was developed in stages by mathematicians who extended and adapted it according to the needs and experiences of industrial as well as academic users. Care was taken to maintain mathematical soundness, and when the language had stabilized, a denotational semantics for it was defined. Subsequently, support tools entirely based on this semantics were and are being developed. We describe the implemented type checker, which gives the sense of directly transliterating the formal type semantics, and preview the proof checker. We discuss the benefits of such a chronology for language and methodology development.