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

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.