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 language | English (US) |
---|---|
Pages (from-to) | 231-245 |
Number of pages | 15 |
Journal | ACM SIGPLAN Notices |
Volume | 37 |
Issue number | 11 |
DOIs | |
State | Published - Nov 2012 |
Externally published | Yes |
Keywords
- Alloy Analyzer
- Alloy modeling language
- Compile-time analysis
- Java language
- Specification language
ASJC Scopus subject areas
- General Computer Science