Internal design of modules specified in the trace assertion method

A software module may be described precisely and completely by a set of related documents: interface specification of the module providing a “black-box” description of its behavior, internal design of the module containing its “clear-box” description, and the code itself. A special formalism is needed in each of these documents. We use the trace assertion method for specification of module interfaces, and LD-relations to specify behavior of individual programs within a module.