property

Each property annotation defines an abstract interpretation over objects in the program. The set of abstract values given in the curly braces form a two-level dataflow lattice. Figure  shows the lattice specified by the Distribution property given in Figure .

  

Figure: Latticed defined by the Distribution property.

Because the lattices are only two levels high, whenever two program paths disagree on the state of an object the resulting meet results in lattice value $\bot$. We are considering ways to allow more complex lattices, such as multiple level lattices or infinite lattices, while still ensuring convergence. The keyword none allows a symbolic name to be assigned to the value $\bot$.