Appendix D                    Specifications

Another way of providing more information about programs is to use formal specifications.  Although this document has largely ignored specifications, Splint 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 Splint checking.  However, LCL specifications can provide more precise documentation on program interfaces than is possible with Splint 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, Tan95] 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 Splint (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.

Specification Flags

These flags are relevant only when Splint is used with LCL specifications.

Global Flags

lcs

Generate .lcs files containing symbolic state of .lcl files (used for imports).  By default .lcs files are generated for each .lcl file processed.  Use -lcs to prevent generation of .lcs files.

lh

Generate .lh files.  By default, -lh is set and no .lh files are generated.  Use +lh to enable .lh file generation. 

i <file>

Set LCL initialization file to <file>.  The LCL initialization file is read if any .lcl files are listed on the command line.  The default file is lclinit.lci, found on the LARCH_PATH.

lclexpect <number>

Exactly <number> specification errors are expected.  Specification errors are errors detected when checking the specifications.  They do not depend on the source code.

Implicit Globals Checking Qualifiers

imp-checked-spec-globs

Implicit checked qualifier on global variables specified in an LCL file with no checking annotation.

imp-checkmod-spec-globs

Implicit checkmod qualifier on global variables specified in an LCL file with no checking annotation.

imp-checkedstrict-spec-globs

Implicit checked qualifier on global variables specified in an LCL file with no checking annotation.

Implicit Annotations

spec-glob-imp-only

Implicit only annotation on global variable declaration in an LCL file with no allocation annotation.

spec-ret-imp-only

Implicit only annotation on return value declaration in an LCL file with no allocation annotation.

spec-struct-imp-only

Implicit only annotation on structure field declarations in an LCL file with no allocation annotation.

spec-imp-only

Sets spec-glob-imp-only, spec-ret-imp-only and spec-struct-imp-only.

Macro Expansion

spec-macros

Macros defining specified identifiers are not expanded and are checked according to the specification. 

Complete Programs and Specifications

spec-undef

Function, variable, iterator or constant specified but never defined.

spec-undecl

Function, variable, iterator or constant specified but never declared.

need-spec

There is information in the specification that is not duplicated in syntactic comments.  Normally, this is not an error, but it may be useful to detect it to make sure checking incomplete systems without the specifications will still use this information.

export-any

An error is reported for any identifier that is exported but not specified.  (Sets all export flags below.)

export-const

Constant exported but not specified.

export-var

Variable exported but not specified.

export-fcn

Function exported but not specified.

export-iter

Iterator exported but not specified.

export-macro

An expanded macro exported but not specified

export-type

Type definition exported but not specified

Next: Appendix E. Annotated Bibliography
Return to Contents