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 only  those things it has to, leaving everything else unmodified, and review  some
attempts at dealing with this ?frame problem? in the Software Specification community.