Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: Paul "E." Black <black@lal.cs.byu.edu>
Date: Mon, 20 Jun 1994 09:30:38 -0600
Message-Id: <9406201530.AA11571@puma.cs.byu.edu>
To: hol2000@leopard.cs.byu.edu
Subject: re: Program Documentation

    Ralf Reetz <reetz@ira.uka.de> writes
	Konrad (konrad@dcs.gla.ac.uk) writes:
	>Question: should the source code to HOL2000 be browsible with mosaic?
	>I imagine that putting all the links in would be a lot of work, but 
	>then again, many users seem to end up perusing the sources (to track 
	>down bugs, reuse code, etc.)
	
	should HOL2000 be made by the use of modern software engineering?
Since the goal of software engineering is to deliver software of
acceptable quality on time, I say, definitely yes!

The first step is to decide the goals of HOL2000.  The appropriate
methods are dependent on the goals or specifications of the project.
Here is my brief estimate as to what is appropriate in each of the
categories mentioned and some additional categories:
	
	- COMPLETE documentation of the source code: description of
	  all data structures, algorithms, functions, module interfaces

This saves errors and wasted time.  Since out-of-date documentation is
generally worse than no documentation, it should be kept brief.

	
	- programmer's style guide line on how to extend HOL2000 using a
	  certain, ``clean'' and uniform programming style

hmmmm, hard to make this useful.  A uniform style is *very* helpful.
Describing the style (both syntactic and semantic) completely leads to
a big document which few would read and (be able to) follow.  So one
or two pages for syntactic style (indentation, positioning of
comments, naming) and five to eight pages for "semantic" style (for
example, error handling, argument checking, language features to use
or void) is probably best.  (see "testing" below)

	
	- COMPLETE documentation of the user interface

I find the book "Introduction to HOL" and Mosaic browsers to be
generally adequate.  Library documentation, though, should be
available via a brower, too.  The best approach seems to be an
automatic LaTex/Postscript to HTML coverter.

	
	- courses and exercises on how to use and extend HOL2000

If you mean from the user level, the more instruction available the
better.  If you mean changing code, I don't think the effort to create
the courses and exercises would be worth the time saved.

	
	- strict revision control

Yes, definitely!  The control need not be restrictive, that is, only a
few people can make changes.  But every change which is made needs:
    the person making the change,
    the date and time, and
    the reason for the change.
Revision control makes it much easier to undo a change which causes a
problem, answer questions like "I thought I fixed that," establish
base lines and working configurations, etc.


	- as independent as possible from certain non-standard features of
	  a certain implementation of the used programming language

Always a good idea.  With the style guide (and perhaps a simple style
checker), nonportable features can be documented and avoided.


	- graphical standard user interface

This is not an attribute of good software engineering per se.  It is a
requirement or specification just like what proof method(s) should be
used or how assumptions are handled.


Something not mentioned above is a thorough test suite.
  * Tests should be as automatic as possible.  That is, one invokes a
	test case or suite with a simple command (rather than
	instructions about typing several lines), and the result
	should be a "Pass" or "Fail-and-here's-why."
  * Any complex, critical, or difficult (history of errors) internal
	function or algorithm should have a built-in self-test, too.
	It is worth writing extra code which just exercises the
	function, to know that there are no known problems with it.
  * Tests and test cases should be developed along with the rest of
	the design.  It leads one to consider cases which otherwise
	might be skipped and does some of the less interesting work
	(writing tests)	at the beginning when energy and enthusiasm is
	typically higher.

Paul E. Black                   Laboratory for Applied Logic
black@lal.cs.byu.edu            3308 TMCB
p.black@ieee.org                Brigham Young University
voice: +1 801 378 8113          Provo, Utah   84602
<A href="http://lal.cs.byu.edu/people/black.html">Mosaic page</A>