test/db3/README

   1      This directory contains the specifications and source code for the
   2 database example in Chapter 5 of ``Larch: Languages and Tools for Formal
   3 Specifications.''  Most of the files in this directory were used to typeset the
   4 figures in Chapter 5.  As a result, they do not adhere to our usual standards
   5 for specifications and code: they lack comments (because they are described in
   6 Chapter 5) and their layout is constrained by the horizontal and vertical space
   7 limitations of the book.
   8
   9      This directory also contains a Makefile, which can serve as a model for
  10 constructing Makefiles that can be used to check the specifications and compile
  11 the code for other programs.
  12
  13      This directory also contains two files, stdio.lcl and file.lsl, which are
  14 not shown in Chapter 5.  These files are the bare beginnings of an approach to
  15 specifying the semantics of the FILE data type in C; they serve little more
  16 than to enable the LCL Checker to check the specifications for db_print in
  17 dbase.lcl.
  18