db: Employee Database Program

The sample uses the employee database program from Appendix B of the Larch
Book:

     Guttag, John V. and Horning, James J., with Stephen J. Garland,
     Kevin D. Jones, Andrs Modet, and Jeannette M. Wing, Larch:
     Languages and Tools for Formal Specification , Springer-Verlag,
     Texts and Monographs in Computer Science, 1993.

An account describing using LCLint 1.2 on the program is found in

     David Evans, Using Specifications to Check Source Code,
     MIT/LCS/TR-628, June 1994.

In each iteration, LCLint is run incrementally on the code and certain
anomalies are detected. The next section fixes these anomalies and runs
LCLint again (sometimes with different flag settings) to detect more
anomalies.

If you want to experiment with the code on your own system, you can also
download the code.

  1. Original version published in the Larch Book
  2. Weak checking on original version with LSL dependancies removed
  3. Using stylized iterators
  4. Standard checking
  5. Memory checking, part 1
  6. Memory checking, part 2
  7. Memory checking, part 3
  8. Checking all macros
  9. Checks mode checking, part 1
 10. Checks mode checking, part 2
 11. Naming conventions
 12. Strict mode checking
 13. Using strict standard library
 14. Final

