Developing and debugging algebraic specifications for Java classes

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Developing and debugging algebraic specifications for Java classes

Full text

Pdf (566 KB)

Source

ACM Transactions on Software Engineering and Methodology (TOSEM) archive
Volume 17 , Issue 3 (June 2008) table of contents

Article No. 14

Year of Publication: 2008

ISSN:1049-331X

Authors

Johannes Henkel	University of Colorado at Boulder, Boulder, CO
Christoph Reichenbach	University of Colorado at Boulder, Boulder, CO
Amer Diwan	University of Colorado at Boulder, Boulder, CO

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 18, Downloads (12 Months): 162, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1363102.1363105 What is a DOI?

ABSTRACT

Modern programs make extensive use of reusable software libraries. For example, a study of a number of large Java applications shows that between 17% and 30% of the classes in those applications use container classes defined in the java.util package. Given this extensive code reuse in Java programs, it is important for the interfaces of reusable classes to be well documented. An interface is well documented if it satisfies the following requirements: (1) the documentation completely describes how to use the interface; (2) the documentation is clear; (3) the documentation is unambiguous; and (4) any deviation between the documentation and the code is machine detectable. Unfortunately, documentation in natural language, which is the norm, does not satisfy the above requirements. Formal specifications can satisfy them but they are difficult to develop, requiring significant effort on the part of programmers.

To address the practical difficulties with formal specifications, we describe and evaluate a tool to help programmers write and debug algebraic specifications. Given an algebraic specification of a class, our interpreter generates a prototype that can be used within an application like a regular Java class. When running an application that uses the prototype, the interpreter prints error messages that tell the developer in which way the specification is incomplete or inconsistent with a hand-coded implementation of the class. We use case studies to demonstrate the usefulness of our system.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	AsmL. //http://research.microsoft.com/fse/asml. Version 2.2.
	2	Glenn Ammons , David Mandelin , Rastislav Bodík , James R. Larus, Debugging temporal specifications with concept analysis, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
	3	Sergio Antoy , Dick Hamlet, Automatically Checking an Implementation against Its Formal Specification, IEEE Transactions on Software Engineering, v.26 n.1, p.55-69, January 2000 [doi>10.1109/32.825766]
	4	Apache Software Foundation. 2003. BCEL—byte code engineering library. http://jakarta.apache.org/bcel/.
	5	Barnett, M., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., and Veanes, M. 2003. Model-based testing with AsmL.NET. In Proceedings of the 1st European Conference on Model-Driven Software Engineering (Dec.)
	6	Beck, K. 2000. Extreme Programming Explained. Addison Wesley.
	7	Beck, Test Driven Development: By Example, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
	8	Huo Yan Chen , T. H. Tse , F. T. Chan , T. Y. Chen, In black and white: an integrated approach to class-level testing of object-oriented programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.7 n.3, p.250-295, July 1998 [doi>10.1145/287000.287004]
	9	Huo Yan Chen , T. H. Tse , T. Y. Chen, TACCLE: a methodology for object-oriented software testing at the class and cluster levels, ACM Transactions on Software Engineering and Methodology (TOSEM), v.10 n.1, p.56-109, Jan. 2001 [doi>10.1145/366378.366380]
	10	Dershowitz, N. and Plaisted, D. A. 2001. Handbook of Automated Reasoning. Vol. 1. Elsevier.
	11	Dershowitz, N. and Vigneron, L. 2003. Database of rewriting systems. http://www.loria.fr/vigneron/RewritingHP/systems.html.
	12	Roong-Ko Doong , Phyllis G. Frankl, The ASTOOT approach to testing object-oriented programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.2, p.101-130, April 1994 [doi>10.1145/192218.192221]
	13	Futatsugi, K. 2003. CafeObj official homepage. http://www.ldl.jaist.ac.jp/cafeobj/.
	14	John Gannon , Paul McMullin , Richard Hamlet, Data Abstraction, Implementation, Specification, and Testing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.3, p.211-223, July 1981 [doi>10.1145/357139.357140]
	15	Goguen, J. 2000. Software Engineering with OBJ: Algebraic Specifications in Action. Kluwer.
	16	Joseph Goguen , Jose Meseguer, Rapid prototyping: in the OBJ executable specification language, ACM SIGSOFT Software Engineering Notes, v.7 n.5, p.75-84, December 1982
	17	Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., and Jouannaud, J.-P. 1993. Introducing OBJ. In Applications of Algebraic Specification using OBJ, J. Goguen, Ed. Cambridge.
	18	Guttag, J. V. and Horning, J. J. 1978. The algebraic specification of abstract data types. Acta Informatica 10, 27--52.
	19	Henkel, J. and Diwan, A. 2003. Discovering algebraic specifications from Java classes. In ECOOP 2003—Object-Oriented Programming, 17th European Conference, L. Cardelli, Ed. Springer, Darmstadt.
	20	Henkel, J. and Diwan, A. 2004a. Case study: Debugging a discovered specification for java.util.arraylist by using algebraic interpretation. Tech. Rep. CU-CS-970-04, University of Colorado at Boulder.
	21	Johannes Henkel , Amer Diwan, A Tool for Writing and Debugging Algebraic Specifications, Proceedings of the 26th International Conference on Software Engineering, p.449-458, May 23-28, 2004
	22	Merlin Hughes , David Stotts, Daistish: systematic algebraic testing for OO programs in the presence of side-effects, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.53-61, January 08-10, 1996, San Diego, California, United States
	23	Daniel Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.2, p.256-290, April 2002 [doi>10.1145/505145.505149]
	24	Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
	25	J. W. Klop, Term rewriting systems, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
	26	Knuth, D. and Bendix, P. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, J. Leech, Ed. Pergamon Press, Oxford, 263--297.
	27	Orna Kupferman , Moshe Y. Vardi, Vacuity Detection in Temporal Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.82-96, September 27-29, 1999
	28	Darko Marinov , Sarfraz Khurshid, VAlloy - Virtual Functions Meet a Relational Language, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right, p.234-251, July 22-24, 2002
	29	John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
	30	Rapanotti, L. and Socorro, A. 1992. Introducing FOOPS. Tech. rep. PRG-TR-28-92, Programming Research Group, Oxford University Computing Laboratory, Oxford.
	31	Sriram Sankar, Run-time consistency checking of algebraic specifications, Proceedings of the symposium on Testing, analysis, and verification, p.123-129, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120818]
	32	Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., and Taghdiri, M. 2003. Debugging overconstrained declarative models using unsatisfiable cores. In 18th IEEE International Conference on Automated Software Engineering (ASE 2003), 6--10 October 2003, Montreal, Canada. IEEE Computer Society, 94--105.
	33	Shlyakhter, I., Sridharan, M., and Jackson, D. 2002. Analyzing Distributed Algorithms with First-Order Logic. http://sdg.csail.mit.edu/pubs/2002/alloy-distalg.pdf.
	34	TeReSe. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press.
	35	J. W. Thatcher , E. G. Wagner , J. B. Wright, Data Type Specification: Parameterization and the Power of Specification Techniques, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.4, p.711-732, Oct. 1982 [doi>10.1145/69622.357192]
	36	Raja Vallée-Rai , Etienne Gagnon , Laurie J. Hendren , Patrick Lam , Patrice Pominville , Vijay Sundaresan, Optimizing Java Bytecode Using the Soot Framework: Is It Feasible?, Proceedings of the 9th International Conference on Compiler Construction, p.18-34, March 25-April 02, 2000
	37	Mark G. J. van den Brand , J. Heering , P. Klint , P. A. Olivier, Compiling language definitions: the ASF+SDF compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.4, p.334-368, July 2002 [doi>10.1145/567097.567099]
	38	Yabo Wang , David Lorge Parnas, Simulating the Behavior of Software Modules by Trace Rewriting, IEEE Transactions on Software Engineering, v.20 n.10, p.750-759, October 1994 [doi>10.1109/32.328996]