Because we have traded off generality for simplicity, our language is limited in the types of abstract interpretation that are supported. For example, our property annotations only allow enumerated lists of values, which correspond to finite lattices. In addition, our lattices have a fixed height of two. These restrictions ensure that our dataflow framework will converge, at the same time hiding the lattice-theoretic foundation of dataflow analysis from the annotator. We anticipate supporting more complex lattices, including integer ranges and restricted classes of infinite lattices. We will enforce termination by putting bounds on the number of iterations of our dataflow analysis.
Our language is also restricted in the sense that there is no way to create dependences between different abstract interpretations.