Aaree: A new approach for modeling object-oriented programs
Aaree presents a veneer onto the first-order relational language Alloy. Alloy is suitable for modeling structural properties of software. Alloy models can be analyzed automatically using the Alloy Analyzer. However, Alloy lacks support for directly modeling object-oriented and imperative constructs. Aaree provides support for several of these constructs; this enables intuitive modeling of object-oriented programs. We give Aaree a formal semantics through a translation to Alloy, which bears resemblance to compilation of OO languages. Since Aaree models can be automatically translated to Alloy, they can also be automatically analyzed using the existing Alloy Analyzer. We illustrate the use of Aaree by modeling a part of the Java Collections Framework. We focus on analyzing properties of views in this framework.
For more information, email khurshid@lcs.mit.edu.
Members
- Sarfraz Khurshid
- Darko Marinov