LSL Traits for using Z with Larch
				  by
			      Hua Zhong

			       Abstract

Z 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.

Keywords: formal methods, specification, Larch, Z, Larch/C++,
mathematical toolkit, debugging

1997 CR Categories:
D.2.1 [Software Engineering]
      Requirements/Specifications -- languages, tools;
F.3.1 [Logics and Meanings of Programs]
      Specifying and Verifying and Reasoning about Programs --
                assertions, invariants, pre- and post-conditions,
                specification techniques.