LSL Traits for using Z with Larch

Abstract

<p>and Larch-style languages are two kind of specification languages that are used for software design. Z is more simple and abstract, while Larch-style behavioral interface specification languages can specify more detail about the interface of a module written in a specific programming language. In this paper, I present Larch Shared Language traits that define the equivalent of the Z mathematical toolkit. These traits can be used by people familiar with the Z mathematical toolkit who wish to write interface specifications in a Larch-style language. I also show how to use these traits to easily translate Z specifications into Larch-style interface specifications. Some of the traits were debugged using the Larch Prover, and I present a description and evaluation of that process, with examples.</p>