This directory contains the specifications and source code for the
database example in Chapter 5 of ``Larch: Languages and Tools for Formal
Specifications.''  Most of the files in this directory were used to typeset the
figures in Chapter 5.  As a result, they do not adhere to our usual standards
for specifications and code: they lack comments (because they are described in
Chapter 5) and their layout is constrained by the horizontal and vertical space
limitations of the book.

     This directory also contains a Makefile, which can serve as a model for
constructing Makefiles that can be used to check the specifications and compile
the code for other programs.

     This directory also contains two files, stdio.lcl and file.lsl, which are
not shown in Chapter 5.  These files are the bare beginnings of an approach to
specifying the semantics of the FILE data type in C; they serve little more
than to enable the LCL Checker to check the specifications for db_print in
dbase.lcl.