Sergey Butkevich
ABSTRACT
We describe an extension to the Java programming language that supports static conformance checking and dynamic debugging of object “protocols,” i.e., sequencing constraints on the order in which methods may be called. Our Java protocols have a statically checkable subset embedded in richer descriptions that can be checked at run time. The statically checkable subtype conformance relation is based on Nierstrasz' proposal for regular (finite-state) process types, and is also very close to the conformance relation for architectural connectors in the Wright architectural description language by Allen and Garlan. Richer sequencing properties, which cannot be expressed by regular types alone, can be specified and checked at run time by associating predicates with object states. We describe the language extensions and their rationale, and the design of tool support for static and dynamic checking and debugging.
- 1.A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading, Massachusetts, 1988. Google Scholar
Digital Library
- 2.R. Allen and D. Garlan. Formalizing architectural connection. In Proceedings of the l Oth ICSE International Conference on Software Engineering, pages 71-80. IEEE, 1994. Google ScholarDigital Library
- 3.R. Allen and D. Garlan. A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology, 6(3):213-249, July 1997. cf. errata in TOSEM 7(3), July 1998. Google ScholarDigital Library
- 4.G. Booch, J. Rumbaugh, and I. Jacobson. The Unified Modeling Language User Guide. Addison-Wesley, Reading, Massachusetts, 1998. Google ScholarDigital Library
- 5.R. H. Campbell and A. N. Habermann. The specification of process synchronization by path expressions. In E. Gelenbe and C. Kaiser, editors, Proceedings of the International Symposium on Operating Systems, volume 16 of Lecture Notes in Computer Science, pages 89-102, Rocquencourt, France, 23-25 April 1974. Springer-Verlag, Berlin, New York. Google ScholarDigital Library
- 6.D. Flanagan. Java in a Nutshell: A Desktop Quick Reference. O'Reilly & Associates, Sebastopol, California, 2nd edition, 1997. Google ScholarDigital Library
- 7.E. Gamma, R. Helm, R. E. Johnson, and J. M. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional Computing Series. Addison-Wesley, Reading, Massachusetts, 1995. Google ScholarDigital Library
- 8.J. Gosling, B. Joy, and G. Steele. The Java Language Specification. The Java Series. Addison-Wesley, Reading, Massachusetts, 1996. Google ScholarDigital Library
- 9.R. B. Kieburtz and A. Silberschatz. Access-right expressions. ACM Transactions on Programming Languages and Systems, 5(1):78-96, Jan. 1983. Google ScholarDigital Library
- 10.R. Kramer. iContract - the Java design by contract tool. In Proceedings of the 1998 on Technology of Object-Oriented Languages and Systems (TOOLS '98), Santa Barbara, California, 3-7 August 1998. Google ScholarDigital Library
- 11.B. H. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6): 1811-1841, 1994. Google ScholarDigital Library
- 12.J. Magee, N. Dulay, S. Eisenbach, and J. Kramer. Specifying distributed software architectures. In Proceedings of the 5th European Software Enginering Conference (ESEC 95), Sitges, Spain, Sept. 1995. Google ScholarDigital Library
- 13.O. Nierstrasz. Regular types for active objects. In Proceedings of the OOPSLA '93 Conference on Object-Oriented Programming Systems, Languages, and Applications, pages 1-15. Association for Computing Machinery, 1993. ACM SIGPLAN Notices, 28(10), October 1993. Google ScholarDigital Library
- 14.K. M. Olender and L. J. Osterweil. Cecil: A sequencing constraint language for automatic static analysis generation. IEEE Transactions on Software Engineering, 16:268-280, Mar. 1990. Google ScholarDigital Library
- 15.K.M. Olender and L. J. Osterweil. Interprocedural static analysis of sequencing constraints. ACM Transactions on Software Engineering and Methodology, 1(1):21-52, Jan. 1992. Google ScholarDigital Library
- 16.C. Peter and E Puntigam. A concurrent object calculus with types that express sequences. In Proceedings of the ECOOP Workshop on Semantics of Objects as Processes (SOAP '99), Lisbon, Portugal, June 1999. Google ScholarDigital Library
- 17.E Puntigam. Types that reflect changes of object usability. In S.Gjesing and K.Nygaard, editors, Proceedings of the Joint Modular Languages Conference (JMLC'97), number 1204 in Lecture Notes in Computer Science, pages 55-77, Linz, Austria, Aug. 1994. Springer-Verlag. Google ScholarDigital Library
- 18.J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, Reading, Massachusetts, 1998. Google ScholarDigital Library
- 19.Sun Microsystems. Java Development Kit, Release 1.1.7. Available at < http ://java.sun.com/products/jdk/1.1/ >.Google Scholar
Index Terms
- Compiler and tool support for debugging object protocols
Recommendations
Compiler and tool support for debugging object protocols
We describe an extension to the Java programming language that supports static conformance checking and dynamic debugging of object “protocols,” i.e., sequencing constraints on the order in which methods may be called. Our Java protocols have a ...
Toward automated abstraction for protocols on branching networks
HLDVT '00: Proceedings of the IEEE International High-Level Validation and Test Workshop (HLDVT'00)We have used various manual abstraction techniques to formally verify a transaction ordering property for an IO protocol over bus/bridge networks. In the context of network protocol verification, an abstraction is needed to reduce the unbounded number ...
Towards automatic debugging of programs
International Conference on Reliable SoftwareWe present the germ of an idea for automatically correcting logical errors in programs by manipulating the invariants of the program. An invariant tree is defined, and we show how it can be used to change the program in order to guarantee correctness.
...
Comments