Institute for Software Research
School of Computer Science, Carnegie Mellon University


Checking Framework Interactions with Relationships

Ciera Jaspan, Jonathan Aldrich

December 2008


Keywords: Software frameworks, relationships, static analysis, verification

Software frameworks impose constraints on how plugins may interact with them. Many of hese constraints involve multiple objects, are temporal, and depend on runtime values. Additionally, they are difficult to specify because they are non-local and may break behavioral subtyping. This work presents relationships as a means for specifying framework constraints, and it presents a formal description and implementation of a static analysis to find constraint violations in plugin code. We define three variants of this analysis: one is sound, one is complete, and one provides compromise of the two. We prove soundness and completeness for the appropriate variants, and we show how the compromise variant works on examples from real-world programs. This allows the user to select the option which is the most cost-effective in practice with regard to the number of false positives and false negatives.

110 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by