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, Andrés 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