An analyzable annotation language

Sarfraz Khurshid, Darko Marinov, Daniel Jackson

Research output: Contribution to journalArticlepeer-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)
Pages (from-to)231-245
Number of pages15
JournalACM SIGPLAN Notices
Issue number11
StatePublished - Nov 2012
Externally publishedYes


  • 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