archives

LSL Traits for using Z with Larch


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Zhong, Hua (1997) LSL Traits for using Z with Larch. Technical Report TR97-22, Department of Computer Science, Iowa State University.

Full text available as:Postscript
Adobe PDF

Abstract

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, 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,
specification techniques.

Subjects:All uncategorized technical reports
ID code:00000170
Deposited by:Staff Account on 08 December 1997



Contact site administrator at: ssg@cs.iastate.edu