[Prev][Next][Index]
Re: Large algebraic specifications
Arie,
One answer to your question is that one shouldn't write 50-page algebraic
specifications, any more than one should write 50-page theorems, or 50-page
predicates, or 50-page function definitions, or 50-page procedures. One
should modularize, and write lots of "little" specifications.
But I will assume that you mean "large collections of little algebraic
specifications that combine in a reasonable way." Under that
interpretation, the Larch Shared Language Handbook almost qualifies as a
50-page specification. It is available in hardcopy in
@book{GHGJMW93,
title = "Larch: Languages and Tools for Formal Specification",
author = "John V. Guttag and James J. Horning,
with S.J. Garland, K.D. Jones, A. Modet,
and J. M. Wing",
year = 1993,
publisher = "Springer-Verlag",
series = "Texts and Monographs in Computer Science",
note = "{ISBN 0-387-94006-5/ISBN 3-540-94006-5}"
}
or (in a slightly updated form) online at URL
http://www.research.digital.com/SRC/larch/toc.html
which gives you a choice of viewing it in PostScript (so you get the nice
TeX operator symbols), or in HTML, so you can click on the links that tie
the little specifications to each other.
We paid a lot of attention in the design of LSL to the issues of scaling
up. I would certainly be interested in your comments on these
specifications, and on the adequacy of the mechanisms we chose for scaling
up.
Other discussion of this and related topics can be found in
@book{MW92,
title = "First International Workshop on Larch, Dedham 1992",
author = "Ursula Martin and Jeannette M. Wing (Eds.)",
year = 1993,
publisher = "Springer-Verlag",
series = "Workshops in Computing",
note = "{ISBN 3-540-19804-0/ISBN 0-387-19804-0}"
}
Jim H.
Follow-Up(s):