Package org.checkerframework.common.accumulation

Class AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy

java.lang.Object
org.checkerframework.framework.type.QualifierHierarchy
org.checkerframework.framework.type.ElementQualifierHierarchy
org.checkerframework.common.accumulation.AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy
Enclosing class:
AccumulationAnnotatedTypeFactory
protected class AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy extends ElementQualifierHierarchy
All accumulation analyses share a similar type hierarchy. This class implements the subtyping, LUB, and GLB for that hierarchy. The lattice looks like: 
       acc()
      /   \
 acc(x)   acc(y) ...
      \   /
     acc(x,y) ...
        |
      bottom
Predicate subtyping is defined as follows:
  • An accumulator is a subtype of a predicate if substitution from the accumulator to the predicate makes the predicate true. For example, Acc(A) is a subtype of AccPred("A || B"), because when A is replaced with true and B is replaced with false, the resulting boolean formula evaluates to true.
  • A predicate P is a subtype of an accumulator iff after converting the accumulator into a predicate representing the conjunction of its elements, P is a subtype of that predicate according to the rule for subtyping between two predicates defined below.
  • A predicate P is a subtype of another predicate Q iff P and Q are equal. An extension point (AccumulationAnnotatedTypeFactory.isPredicateSubtype(String, String)) is provided to allow more complex subtyping behavior between predicates. (The "correct" subtyping rule is that P is a subtype of Q iff P implies Q. That rule would require an SMT solver in the general case, which is undesirable because it would require an external dependency. A user can override AccumulationAnnotatedTypeFactory.isPredicateSubtype(String, String) if they require more precise subtyping; the check described here is overly conservative (and therefore sound), but not very precise.)