analyze

Each library procedure can have a set of analyze annotations that describe how that procedure affects the properties of the objects it manipulates. Collectively, these annotations compose the dataflow transfer function for each abstract interpretation. Each statement in this annotation behaves as a logical implication: if the conditions on the left of the => operator are true, then we conclude that the facts on the right are true. Each term in the condition is limited to testing the current property value of an object, or comparing to a constant. Each condition is a logic expression made up of these terms. In the absence of the => operator, the facts are assumed without condition.

The PLAPACK annotations in Figure  show several examples of the analyze annotation. The part labeled (5) describes the effect of a vertical split on the distribution of various input view types. The matrix multiply procedure, PLA_Gemm, analyzes the contents of the matrices involved. For example, it expresses the fact that multiplying two upper-triangular matrices yields an upper-triangular matrix as a result.

When more than one analysis statement applies, the most specific one is chosen: the statement with the greatest number of conditions that are true, minus any that are false. For example, given an analyze annotation of the follow form:

analyze Foo {
  (A)      => C1;
  (A && B) => C2;
  (A || B) => C3;
}

If only A is true, then we would conclude C1. If both A and B are true, then we choose either C2 or C3. Ties are broken by preferring the statement that occurs earlier in the annotation.