horning@src.dec.com (Jim Horning) (07/11/90)
The following report is now available. Single copies at no charge may be requested by sending mail to src-report@src.dec.com. DEC Systems Research Center Report 60, July 4, 1990 "Debugging Larch Shared Language Specifications" Stephen J. Garland, John V. Guttag, James J. Horning ABSTRACT: The Larch family of specification languages supports a two-tiered definitional approach to specification. Each specification has components written in two languages: one designed for a specific programming language and another independent of any programming language. The former are called Larch interface languages, and the latter the Larch Shared Language (LSL). The Larch style of specification emphasizes brevity and clarity rather than executability. To make it possible to test specifications without executing or implementing them, Larch permits specifiers to make claims about logical properties of specifications and to check these claims at specification time. Since these claims are undecidable in the general case, it is impossible to build a tool that will automatically certify claims about arbitrary specifications. However, it is feasible to build tools that assist specifiers in checking claims as they debug specifications. This paper describes the checkability designed into LSL and discusses two tools that help perform the checking. This paper will appear in the forthcoming IEEE TSE Special Issue on Formal Methods. It is a revised and expanded version of a paper presented at the April 1990 IFIP Working Conference on Programming Concepts and Methods.