An analyzable annotation language

Sarfraz Khurshid, Darko Marinov, Daniel Jackson

Research output: Contribution to conferencePaperpeer-review


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)
Number of pages15
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


Conference17th ACM Conference on Object-Orientated Programming Systems, Languages, and Applications
Country/TerritoryUnited States
CitySeattle, WA


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

ASJC Scopus subject areas

  • General Computer Science


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

Cite this