Zhong, Hua (1997) LSL Traits for using Z with Larch. Technical Report TR97-22, Department of Computer Science, Iowa State University.
LSL Traits for using Z with Larch
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, Lrch/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,
Contact site administrator at: firstname.lastname@example.org