Abstract

Completeness is usually listed as a desirable attribute of specifications; incompleteness, as a reason for the failure of software to satisfy its intended requirements. Unfortunately, these terms are rarely given anything but intuitive definitions, making it unclear how to achieve the former or, alternatively, avoid the latter. This thesis begins by examining various notions of (in)completeness in specifications, and introduces a pragmatic definition of incompleteness: a classification based on its potential sources. From this, it observes that completeness, though needed to properly reason about, and capture the behaviour of, the system, is undesirable in some cases. To reconcile these conflicting needs, this thesis proposes a novel formal method for (partially) tolerating incompleteness in specifications. The method focuses on one of the classes. A connection is drawn between this class and a group of related problems involved in reasoning about time and action in artificial intelligence: the qualification, frame, and ramification problems. Both endeavors must contend with incomplete information. Since the techniques employed to deal with these problems usually involve non-monotonic logics, a number of such logics are considered, but most rejected. Shoham's logic of chronological ignorance, however, shows promise. Its shortcomings are addressed, and an extension of it defined. This serves as the formal basis for the specification language KAT, which is intended for real-time, concurrent systems. The thesis concludes with a description of the language, a discussion of pragmatic issues, including how it permits fairly easy modification of specifications, and a specification of a telephone system demonstrating its use