Final Version

Changes from Strict Library

Fixed errors reported using strict library.

Now, running LCLint detects no anomalies.

Modules

employee - employee datatype (LCL, Code, Header)
empset - sets of employees (LCL, Code, Header)
dbase - database of employees (LCL, Code, Header)
eref - reference to an employee (LCL, Code, Header)
erc - collection of erefs (LCL, Code, Header)
ereftab - table of employees and erefs (LCL, Code, Header)

Summary

We've just about reached the limit of what can be done usefully with LCLint 2.0. In the course of checking, we have discovered a number of bugs in the code, enhanced missing or incomplete specifications, improved the documentation by adding annotations, adopted a naming convention, and checked the code against a stricted version of the standard library.

Although this is a toy example, it closely mirrors how LCLint has been used to find real problems in large programs.

If we are still unsatisfied with the trustworthiness of the code, we could:

Add claims to the LCL specifications and use LP to prove they are correct.
Use run-time checking tools.

Return to Summary