An analyzable annotation language
An analyzable annotation language
复制标题
可分析的注释语言
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
D. Jackson
中科院分区：
文献类型：
--
作者：
S. Khurshid;D. Marinov;D. Jackson
合金注释语言（AAL）是一种基于合金建模语言注释Java代码的语言（正在开发）。它提供了类似于Java建模语言（JML）的语法，并提供了生成运行时间断言的机会。但是，AAL还提供了全自动编译时间分析的可能性。支持几种分析，包括：根据其规范检查方法的代码；检查子类中方法的规范是否与超类中的规范兼容；并检查有关方法对不同对象的调用的属性，例如，等于类的方法（及其覆盖物）会引起等效性。使用部分模型代替代码，还可以在摘要中分析面向对象的设计：例如，调查对象之间的视图关系。论文提供了注释和此类分析的示例。它（非正式地）将注释的系统翻译成合金，该合金是一种具有关系运算符的简单一阶逻辑。通过这样做，它使Alloy的自动分析基于最先进的SAT求解器，适用于面向对象的程序的分析，并演示了简单逻辑作为注释语言的基础。
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.