TY - JOUR
T1 - An analyzable annotation language
AU - Khurshid, Sarfraz
AU - Marinov, Darko
AU - Jackson, Daniel
N1 - Funding Information:
We would like to thank Matthias Felleisen, Viktor Kuncak, and Gregory Sullivan for discussions on AAL and comments on an earlier draft of this paper. This work was funded in part by ITR grant #0086154 from the National Science Foundation.
Publisher Copyright:
© 2002 ACM
PY - 2012/11
Y1 - 2012/11
N2 - 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.
AB - 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.
KW - Alloy Analyzer
KW - Alloy modeling language
KW - Compile-time analysis
KW - Java language
KW - Specification language
UR - http://www.scopus.com/inward/record.url?scp=85062229607&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85062229607&partnerID=8YFLogxK
U2 - 10.1145/583854.582441
DO - 10.1145/583854.582441
M3 - Article
AN - SCOPUS:85062229607
SN - 1523-2867
VL - 37
SP - 231
EP - 245
JO - ACM SIGPLAN Notices
JF - ACM SIGPLAN Notices
IS - 11
ER -