Data groups: specifying the modification of extended state

ABSTRACT

This paper explores the interpretation of specifications in the context of an object-oriented programming language with subclassing and method overrides. In particular, the paper considers annotations for describing what variables a method may change and the interpretation of these annotations. The paper shows that there is a problem to be solved in the specification of methods whose overrides may modify additional state introduced in subclasses. As a solution to this problem, the paper introduces data groups, which enable modular checking and rather naturally capture a programmer's design decisions.

REFERENCES

• AdB94: Pierre America and Frank de Boer. Reasoning about dynamically evolving process structures. Formal Aspects of Computing, 60):269- 316, 1994.
• AL97: Martín Abadi , K. Rustan M. Leino, A Logic of Object-Oriented Programs, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.682-696, April 14-18, 1997
• CBS98: Edwin C. Chan , John T. Boyland , William L. Scherlis, Promises: limited specifications for analysis and manipulation, Proceedings of the 20th international conference on Software engineering, p.167-176, April 19-25, 1998, Kyoto, Japan
• Det96: David L. Detlefs. An overview of the Extended Static Checking system. In Proceedings of The First Workshop on Formal Methods in Software Practice, pages 1-9. ACM SIGSOFT, January 1996.
• DLN98: David L. Detlefs, K. Rustan M. Leino, and Greg Nelson. Wrestling with rep exposure. Research Report 156, Compaq Systems Research Center, 1998.
• DLNS98: David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, 1998. To appear.
• ESC: Extended Static Checking home page, Compaq Systems Research Center. On the Web at www. research, digital, corn/SRC/esc /Esc. html.
• GH93: John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
• Hoa72: C.A.R. Hoare. Proof of correcmess of data representations. Acta Informatica, 1(4):271-81, 1972.
• Jac95: Daniel Jackson, Aspect: detecting bugs with abstract dependences, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.2, p.109-145, April 1995 [doi>10.1145/210134.210135]
• Jon91: H. B. M. Jonkers, Upgrading the Pre- and Postcondition Technique, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.428-456, October 21-25, 1991
• Lam93: John Lamping, Typing the specialization interface, ACM SIGPLAN Notices, v.28 n.10, p.201-214, Oct. 1, 1993
• LB97: Gary T. Leavens and Albert L. Baker. Enhancing the pre- and postcondition technique for more expressive specifications. Technical Report TR #97-19, Department of Computer Science, Iowa State University, September 1997.
• Lea89: Gary Todd Leavens. Verifying Object-Oriented Programs that Use Subtypes. PhD thesis, MIT Laboratory for Computer Science, February 1989. Available as Technical Report MIT/LCS~-439.
• Lea96: Gary T. Leavens. An overview of Larch/C++: Behavioral specifications for C++ modules. In Haim Kilov and William Harvey, editors, Specification of Behavioral Semantics in Object- Oriented information Modeling, chapter 8, pages 121-142. Kluwer Academic Publishers, 1996.
• Lei95: K. Rustan Leino, Toward reliable modular programs, California Institute of Technology, Pasadena, CA, 1995
• Lei97: K. Rustan M. Leino. Ecstatic: An objectoriented programming language with an axiomatic semantics. In The Fourth International Workshop on Foundations of Object- Oriented Languages, January 1997. Proceedings available from www. cs. indiana, edu /hyplan/pierce/fool/.
• Lei98a: K. Rustan M. Leino, Recursive Object Types in a Logic of Object-Oriented Programs, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.170-184, March 28-April 04, 1998
• Lei98b: K. Rustan M. Leino. Specifying the modification of extended state. In The Fifth International Workshop on Foundations of Object- Oriented Languages, January 1998. Proceedings available from www.pauillac, inria . fr/~ remy/fool/program, html.
• LH94: K. Lano , H. Haughton, Object-oriented specification case studies, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• LN98a: K. Rustan M. Leino and Greg Nelson. Abstraction and specification revisited. Internal manuscript KRML 71, Digital Equipment Corporation Systems Research Center. To appear as Compaq SRC Research Report 160, 1998.
• LN98b: K. Rustan M. Leino , Greg Nelson, An Extended Static Checker for Modular-3, Proceedings of the 7th International Conference on Compiler Construction, p.302-305, March 28-April 04, 1998
• LS97: K. Rustan M. Leino and Raymie Stata. Checking object invariants. Technical Note 1997- 007, Digital Equipment Corporation Systems Research Center, April 1997.
• LW94: Barbara H. Liskov , Jeannette M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1811-1841, Nov. 1994 [doi>10.1145/197320.197383]
• Mey88: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• Nau94: David A. Naumann, Predicate Transformer Semantics of an Oberon-Like Language, Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi, p.467-487, June 06-10, 1994
• PHM98: Arnd Poetzsch-Heffter , Peter Müller, Logical foundations for typed object-oriented languages, Proceedings of the IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods, p.404-423, June 08-12, 1998
• Sta97: R. Stata, Modularity in the Presence of Subclassing, Massachusetts Institute of Technology, Cambridge, MA, 1997
• Van94: Mark T. Vandevoorde, Exploiting specifications to improve program performance, Massachusetts Institute of Technology, Cambridge, MA, 1993

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Object-oriented languages

General Terms:
Design, Languages, Performance, Theory