[Prev][Next][Index]

VDM and Z handbooks in LSL

One thing that makes Larch-style and VDM and Z specifications
hard to compare is the differing mathematical vocabulary.
I suggest that some enterprising student could make a good
master's project out of defining a handbook of LSL traits
that would mimic the vocabulary of VDM, and another one for Z.
(The VDM project would be simplier, Z I think has more vocabulary.)
A lot of this would probably be just a simple adaptation
of the traits already in Guttag and Horning's LSL handbook.

Such a project would offer additional advantages,
besides the academic interest of easing comparisons between
rival ways of specifying something:

	- often users of a specification language don't want
	  to write their own traits, and would be happy
	  using combinations of sets, tuples, etc.

	- one could more easily translate existing VDM
	  or Z specifications into a Larch-style language,
	  such as LM3, LCL, Larch/C++, etc.

In terms of comparing specification languages, such a set of
handbooks would do away with the (incorrect) argument that one
has to always specify a new trait in LSL in order to write
an interface specification using a Larch-style interface
specification language.

I had suggested such a project to a graduate student here,
but he decided to do something else.  Since I have no
immediate prospects of anyone doing this at Iowa State,
I offer it to anyone else that is intersted, because I think
it's important in advancing the utility of the Larch family
of languages.

(I'd be happy to be on the appropriate thesis committee,
if that would help.  Or, if some company wants to fund
a student to do it, I'm sure I can get someone to do it here!)

	Gary Leavens

--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/homepage.html