An analyzable annotation language

Sarfraz Khurshid, Darko Marinov, Daniel Jackson

Research output: Contribution to conferencePaperpeer-review

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.

Original languageEnglish (US)
Pages231-245
Number of pages15
DOIs
StatePublished - 2002
Externally publishedYes
Event17th ACM Conference on Object-Orientated Programming Systems, Languages, and Applications - Seattle, WA, United States
Duration: Nov 4 2002Nov 8 2002

Other

Other17th ACM Conference on Object-Orientated Programming Systems, Languages, and Applications
CountryUnited States
CitySeattle, WA
Period11/4/0211/8/02

Keywords

  • Alloy analyzer
  • Alloy modeling language
  • Compile-time analysis
  • Java language
  • Specification language

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'An analyzable annotation language'. Together they form a unique fingerprint.

Cite this