Re: Large algebraic specifications

horning@pa.dec.com wrote:
: 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.
:   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.

In the ideal case - you write 5 "little" specifications that refer
to pre-existing specifications.  By using the above technology
these references can be
links so that the readers can instantly (or at least quickly)
see the specs you are using if they need to know the details.

For example.... you should be able to say that you will be
assuming the set of positions of an elevator forms a linearly ordered
set (in your chosen notation) and have a link created to a standard
definition that has been filed on the internet.  Perhaps like this:
.See http://www.csci.csusb.edu/dick/maths/math_21_Order.html#Loset

We have the technology to make specifications much smaller.

What we do not have is a standard collection of linkable
building blocks.  We don't even have a name for what such a thing would
be, it would be a mixture of a data-base, a knowledge-base, data dictionary,
an encyclopedia of mathematics, and a repository.

I have an experimental prototype at
or use FTP
to access

Find out what's new at http://www.csci.csusb.edu/doc/www.sites.html
Disclaimer:`CSUSB may or may not agree with this message`.
Copyright(1995):Copy this freely but include the following link to the
<a href="http://www.csci.csusb.edu/dick/signature.html">author's signature</a>