This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
On the Frame Problem in Procedure Specifications
October 1995 (vol. 21 no. 10)
pp. 785-798
The paper provides 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. The second part of the paper adapts a recent proposal for a solution to the frame problem in Artificial Intelligence—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, its semantics is relatively straight-forward. The paper also suggests an algorithm which generates syntactically the explanation closure axioms from the pre/postcondition specifications, provided they are written in a restricted language; it also suggests a model theory supporting it.

[1] A.J. Alencar and J.A. Goguen,“Specification in OOZE with examples,” K. Lanno and H. Haughton, eds., Object-Oriented Specification Case Studies.Englewood Cliffs, N.J.: Prentice Hall, 1994, pp. 158-183.
[2] A. Auernheimer and R. Kemmerer,“Procedural and nonprocedural semantics of the ASLAN formal specification language,” Proc. 19th Hawaii Int’l Conf. on System Sciences (HICS), 1986, pp.784-794.
[3] A. Borgida,“On the definition of specialization hierarchies for procedures,” Proc. IJCAI’81,Vancouver, B.C., Canada, Aug. 1981, pp. 254-256.
[4] A. Borgida,J. Mylopoulos,, and H.K.T. Wong,“Generalization/specialization as a basis for software specification,” M. Brodie, J. Mylopoulos, and J. Schmidt, eds., On Conceptual Modeling: Perspectives From Artificial Intelligence, Databases and Programming Languages.New York: Springer Verlag, 1984, pp. 87-114.
[5] A. Borgida,J. Mylopoulos,J. Schmidt,, and I. Wetzel,“Support for data-intensive applications: Conceptual design and software development,” R. Hull, R. Morrison, and D. Stemple, eds., Database Programming Languages.San Mateo, Calif.: Morgan Kaufmann Publishers, 1990.
[6] B. Cohen,W.T. Harwood,, and M.I. Jackson,The Specification of Complex Systems.Reading, Mass.: Addison Wesley, 1986.
[7] D. Duke and R. Duke,“Towards a semantics for object Z,” VDM and Z—Formal Methods in Software Development, Lecture Notes in Computer Science, vol. 428. Berlin: Springer Verlag, 1990, pp. 244-261.
[8] J. Guttag,J.J. Horning,, and J.W. Wing,“Larch in five easy pieces,” TR 5, DEC Systems Research Center, 1985.
[9] A.R. Haas,“The case for domain specific frame axioms,” F.M. Brown, ed., The Frame Problem in Artificial Intelligence: Proceedings of the 1987 Workshop.San Mateo Calif.: Morgan Kaufmann Publishers, Inc., 1987, pp. 343-348.
[10] J. Haugelstein and D. Roclants,“Reconciling operational and declarative specifications,” Proc. Int’l Conf. on Advanced Information Systems Engineering (CAiSE).Manchester, England, May12-15, 1992.
[11] C.B. Jones, Systematic Software Development Using VDM.Englewood Cliffs, N.J.: Prentice Hall, 1986.
[12] H.B.M. Jonkers,“Updating the pre- and postcondition technique,” VDM’91 Formal Software Development Methods, Lecture Notes in Computer Science. New York: Springer Verlag, 1991, pp. 428-456.
[13] K. Lano and H. Haughton, eds., Object-Oriented Specification Case Studies.Englewood Cliffs, N.J.: Prentice Hall, 1993.
[14] V. Lifschitz,“Toward a metatheory of action,” Proc. Second Int’l Conf. on Principles of Knowledge Representation and Reasoning (KR’91).San Mateo, Calif.: Morgan Kaufmann Publishers, Inc., 1991, pp. 376-386.
[15] F. Lin and Y. Shoham,“Provably correct theories of action,” Proc. Nat’l Conf. on Artificial Intelligence, 1991.
[16] F. Lin and R. Reiter,“State constraints revisited,” J. of Logic and Computation, vol. 4, pp. 655-678, 1994.
[17] L. Marshall and L. Simon,“Using VDM within an object-oriented framework,” VDM and Z—Formal Methods in Software Development, Lecture Notes in Computer Science, vol. 428. New York: Springer Verlag, 1991.
[18] J. McCarthy,“Situations, actions, and causal laws,” technical report, Stanford University, 1963; also reprinted in M. Minsky, ed., Semantic Information Processing.Cambridge, Mass.: MIT Press, 1968.
[19] J. McCarthy and P. Hayes,“Some philosophical problems from the standpoint of artificial intelligence,” B. Melzter and D. Michie, eds., Machine Intelligence 4.Edinburgh: Edinburgh Univ. Press, 1969, pp. 463-502.
[20] J. McCarthy, "Applications of Circumscription to Formalising Commonsense Knowledge," Artificial Intelligence, vol. 28, pp. 89-116, 1986.
[21] B. Meyer,Object-Oriented Software Construction. Englewood Cliffs, NJ: Prentice-Hall, 1988.
[22] J. Mylopoulos, P. Bernstein, and H. Wong, “A Language Facility for Designing Interactive, Database-Intensive Applications,” ACM Trans. Database Systems, vol. 5, no. 2, 1980.
[23] E.P.D. Pednault,“ADL: Exploring the middle ground between STRIPS and the situation calculus,” Proc. First Int’l Conf. on Principles of Knowledge Representation and Reasoning (KR’89).San Mateo, Calif.: Morgan Kaufmann Publishers Inc., 1989, pp. 324-332.
[24] D. A. Penny, R. C. Holt, and M. W. Godfrey,“Formal specification in metamorphic programming,”inVDM '91, 4th Int. Symp. VDM Europe Proc.New York: Springer-Verlag, 1991.
[25] D. E. Perry,“The Inscape environment,”inProc. 11th Int. Conf. Software Eng., IEEE Computer Society, May 1989, pp. 2–12.
[26] R. Reiter,“Nonmonotonic reasoning,” Annual Review of Computer Science 2, Annual Reviews Inc., 1987, pp. 147-186.
[27] R. Reiter,“The frame problem in the situation calculus: A simple solution(sometimes) and a completeness result for goal regression,” V. Lifschitz, ed., Artificial Intelligence and the Mathematical Theory of Computation: Papers in Honor of John McCarthy.San Diego, Calif.: Academic Press, 1991, pp. 359-380.
[28] R. Reiter,“On specifying database updates,” J. of Symbolic Programming (to appear).
[29] M. Ryan,J. Fiadeiro,, and T. Maibaum,“Sharing actions and attributes in modal action logic,” Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, no. 526. New York: Springer Verlag, 1991, pp. 569-593.
[30] K.-D. Schewe,J. W. Schmidt,, and I. Wetzel,“Specification and refinement in an integrated database application environment,” VDM’91—Formal Software Development Methods, Lecture Notes in Computer Science. New York: Springer Verlag, 1991, pp. 496-510.
[31] L.K. Schubert,“Monotonic solution of the frame problem in the situation calculus: Anefficient method for worlds with fully specified actions,” H.E. Kyberg, R.P. Loui, and G.N. Carlson, eds., Knowledge Representation and Defeasible Reasoning. Kluwer Academic Press, 1990, pp. 23-67.
[32] S.A. Schuman, and D.H. Pitt,“Object-oriented subsystem specification,” L.G.L.T. Meertens, ed, Program Specification and Transformation.North Holland, 1987, pp. 313-341.
[33] J. M. Spivey,The Z Notation: A Reference Manual. Englewood Cliffs, NJ: Prentice-Hall, 1989.
[34] S. Stepney, R. Barden, and D. Cooper, eds., Object Orientation in Z, Workshops in Computing Series. New York: Springer Verlag, 1992.

Index Terms:
Formal, specifications, languages, frame assertion, proof obligations, semantics of specification languages, inheritance.
Citation:
Alex Borgida, John Mylopoulos, Raymond Reiter, "On the Frame Problem in Procedure Specifications," IEEE Transactions on Software Engineering, vol. 21, no. 10, pp. 785-798, Oct. 1995, doi:10.1109/32.469460
Usage of this product signifies your acceptance of the Terms of Use.