third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/AbstractValue.java


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

package org.checkerframework.dataflow.analysis;

/**
 * An abstract value used in the org.checkerframework.dataflow analysis.
 *
 * @author Stefan Heule
 *
 */
public interface AbstractValue<V extends AbstractValue<V>> {

    /**
     * Compute the least upper bound of two stores.
     *
     * <p>
     *
     * <em>Important</em>: This method must fulfill the following contract:
     * <ul>
     * <li>Does not change {@code this}.</li>
     * <li>Does not change {@code other}.</li>
     * <li>Returns a fresh object which is not aliased yet.</li>
     * <li>Returns an object of the same (dynamic) type as {@code this}, even if
     * the signature is more permissive.</li>
     * <li>Is commutative.</li>
     * </ul>
     */
    V leastUpperBound(V other);
}