]>
Commit | Line | Data |
---|---|---|
885824d3 | 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 |