SLIC: A Specification Language for Interface Checking (of C)

Modern software systems are built by a multitude of programmers using application program interfaces (APIs). When a software system is built using APIs, there are several classes of problems that can hamper its dependability: a client P of an API may use it improperly; an implementation L may not properly implement the API. There are many requirements on both the client and implementer of an API that are typically stated only in the documentation for the API. Currently, only a small portion of these requirements |namely, the number of arguments of a function, and the types of each argument and return value| are stated in the header file for the API and checked for agreement at call sites by the compiler. We wish to express temporal safety requirements [15] on the API, such as rules about ordering of function calls with associated constraints on the data values visible at the API boundary, and automatically check (statically or dynamically) if these requirements are satisfied by the client and the implementer of the API.