″And nothing else″: the frame problem in procedure specifications

Alex Borgida, John Mylopoulus, Raymond Reiter

Research output: Chapter in Book/Report/Conference proceedingConference contribution

23 Scopus citations


We give examples of situations where formal specifications of procedures in the standard pre/postcondition style become lengthy, cumbersome and difficult to change, a problem which is particularly acute in the case of object-oriented specifications with inheritance. We identify the problem as the inability to express that a procedure ″changes nothing else (unless otherwise explicitly stated)″. We then review various attempts at dealing with the problem in the Software Specification community, and relate it to the twenty-year old frame problem in the field of Artificial Intelligence. The second part of the paper adapts a recent proposal for a solution to the frame problem --- the notion of explanation closure axioms --- to provide an approach whereby one can state such conditions succinctly and modularly, with the added advantage of having the specifier be reminded of things that she may have omitted saying in procedure specifications. Since this approach is based on standard Predicate Logic, it does not require the development of special purpose theorem provers. The paper also outlines an algorithm which generates syntactically the explanation closure axioms from the pre/postcondition specifications, provided they are written in a restricted language.

Original languageEnglish (US)
Title of host publicationProceedings - International Conference on Software Engineering
PublisherPubl by IEEE
Number of pages12
ISBN (Print)0818637005
StatePublished - 1993
EventProceedings of the 15th International Conference on Software Engineering - Baltimore, MD, USA
Duration: May 17 1993May 21 1993

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257


OtherProceedings of the 15th International Conference on Software Engineering
CityBaltimore, MD, USA

All Science Journal Classification (ASJC) codes

  • Software


Dive into the research topics of '″And nothing else″: the frame problem in procedure specifications'. Together they form a unique fingerprint.

Cite this