LCLint User's Guide - Appendix G: Specifications

Appendix G Specifications

Another way of providing more information about programs is to use formal specifications. Although this document has largely ignored specifications, LCLint was originally designed to use the information in LCL specifications instead of source-code annotations. This document focuses on annotations since it takes less effort to add annotations to source code than to maintain an additional specification file. Annotations can express everything that can be expressed in LCL specifications that is relevant to LCLint checking. However, LCL specifications can provide more precise documentation on program interfaces than is possible with LCLint annotations. This appendix (extracted from [Evans94]) is a very brief introduction to LCL Specifications. For more information, consult [GH93].

The Larch family of languages is a two-tiered approach to formal specification. A specification is built using two languages -- the Larch Shared Language (LSL), which is independent of the implementation language, and a Larch Interface Language designed for the specific implementation language. An LSL specification defines sorts, analogous to abstract types in a programming language, and operators, analogous to procedures. It expresses the underlying semantics of an abstraction.

The interface language specifies an interface to an abstraction in a particular programming language. It captures the details of the interface needed by a client using the abstraction and places constraints on both correct implementations and uses of the module. The semantics of the interface are described using primitives and sorts and operators defined in LSL specifications. Interface languages have been designed for several programming languages.

LCL [GH93, Tan94] is a Larch interface language for Standard C. LCL uses a C-like syntax. Traditionally, a C module M consists of a source file, M.c, and a header file, M.h. The header file contains prototype declarations for functions, variables and constants exported by M, as well as those macro definitions that implement exported functions or constants, and definitions of exported types. When using LCL, a module includes two additional files - M.lcl, a formal specification of M, and M.lh, which is derived by LCLint (if the lh flag is on) from M.lcl. Clients use M.lcl for documentation, and should not need to look at any implementation file. The derived file, M.lh, contains include directives (if M depends on other specified modules), prototypes of functions and declarations of variables as specified in M.lcl. The file M.h should include M.lh and retain the implementation aspects of the old M.h, but is no longer used for client documentation.