An analyzable annotation language

ABSTRACT

The Alloy Annotation Language (AAL) is a language (under development) for annotating Java code based on the Alloy modeling language. It offers a syntax similar to the Java Modeling Language (JML), and the same opportunities for generation of run-time assertions. In addition, however, AAL offers the possibility of fully automatic compile-time analysis. Several kinds of analysis are supported, including: checking the code of a method against its specification; checking that the specification of a method in a subclass is compatible with the specification in the superclass; and checking properties relating method calls on different objects, such as that the equals methods of a class (and its overridings) induce an equivalence. Using partial models in place of code, it is also possible to analyze object-oriented designs in the abstract: investigating, for example, a view relationship amongst objects.The paper gives examples of annotations and such analyses. It presents (informally) a systematic translation of annotations into Alloy, a simple first-order logic with relational operators. By doing so, it makes Alloy's automatic analysis, which is based on state-of-the-art SAT solvers, applicable to the analysis of object-oriented programs, and demonstrates the power of a simple logic as the basis for an annotation language.

REFERENCES

• 1: Kent Beck, Extreme programming explained: embrace change, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 2: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
• 3: M. Dalal and D. Gangopahyay. OOLP: A translation approach to object-oriented logic programming. In Proc. First International Conference on Deductive and Object-Oriented Databases (DOOD-89), pages 555--568, Kyoto, Japan, Dec. 1989.
• 4: D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, 1998.
• 5: Jay Earley, Toward an understanding of data structures, Communications of the ACM, v.14 n.10, p.617-627, Oct. 1971 [doi>10.1145/362759.362764]
• 6: Robert Bruce Findler , Matthias Felleisen, Contract Soundness for object-oriented languages, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.1-15, October 14-18, 2001, Tampa Bay, FL, USA
• 7: Richard Helm , Ian M. Holland , Dipayan Gangopadhyay, Contracts: specifying behavioral compositions in object-oriented systems, Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, p.169-180, September 1990, Ottawa, Canada
• 8: M. Huisman, B. Jacobs, and J. van den Berg. A case study in class library verification: Java's Vector class. Software Tools for Technology Transfer, 2001.
• 9: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 10: D. Jackson. Micromodels of software: Modelling and analysis with Alloy, 2001. Available online: http://sdg.lcs.mit.edu/alloy/book.pdf.
• 11: 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]
• 12: Daniel Jackson, Object models as heap invariants, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
• 13: Daniel Jackson , Alan Fekete, Lightweight Analysis of Object Interactions, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.492-513, October 29-31, 2001
• 14: Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 15: 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
• 16: Idit Keidar , Roger Khazan , Roger I. Khazan , Nancy Lynch , Alex Shvartsman, An inheritance-based technique for building simulation proofs incrementally, Proceedings of the 22nd international conference on Software engineering, p.478-487, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337358]
• 17: Viktor Kuncak , Patrick Lam , Martin Rinard, Role analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.17-32, January 16-18, 2002, Portland, Oregon
• 18: G. T. Leavens. An overview of Larch/C++: Behavioral specifications for C++ modules. In H. Kilov and W. Harvey, editors, Specification of Behavioral Semantics in Object-Oriented Information Modeling, pages 121--142. Kluwer Academic Publishers, 1996.
• 19: G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University, June 1998. (last revision: Aug 2001).
• 20: K. Rustan M. Leino, Data groups: specifying the modification of extended state, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.144-153, October 18-22, 1998, Vancouver, British Columbia, Canada
• 21: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 22: D. C. Luckham and F. von Henke. An overview of Anna, a specification language for Ada. In IEEE Software, volume 2, pages 9--23, Mar. 1985.
• 23: Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 24: Darko Marinov , Sarfraz Khurshid, TestEra: A Novel Framework for Automated Testing of Java Programs, Proceedings of the 16th IEEE international conference on Automated software engineering, p.22, November 26-29, 2001
• 25: 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
• 26: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 27: Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.221-231, June 2001, Snowbird, Utah, United States
• 28: Chris Moss, Prolog++: The Power of Object-Oriented and Logic Programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1994
• 29: P. Muller, A. Poetzsch-Heffter, and G. T. Leavens. Modular specification of frame properties in JML. Technical Report 02-02, Iowa State University, Feb. 2002.
• 30: M. Roulo. How to avoid traps and correctly override methods from JLO. http://www.javaworld.com/javaworld/jw-01-1999/jw-01-object.html.
• 31: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 32: The Object-Z specification language, Kluwer Academic Publishers, Norwell, MA, 1999
• 33: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• 34: Sun Microsystems. Java 2 Platform, Standard Edition, v1.3.1 API Specification. http://java.sun.com/j2se/1.3/docs/api/.
• 35: Joachim van den Berg , Bart Jacobs, The LOOP Compiler for Java and JML, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.299-312, April 02-06, 2001
• 36: M. Vaziri. Finding bugs with a constraint solver. PhD Thesis Proposal, Dept. of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA, 2002.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Programming by contract; Class invariants

General Terms:
Languages, Verification

Keywords:
alloy analyzer, alloy modeling language, compile-time analysis, java language, specification language