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

	Splint - Secure Programming Lint evans@virginia.edu Download - Documentation - Manual - Links Source - Linux - Publications - Talks Reporting Bugs    Sponsors - Credits