GeezerVison

The variable has a value greater than zero.

@Refinement("positive > 0")
int positive;
positive = 50;   // Correct
positive = -1;   // Error

Lower and upper bounds set on a variable. The _ wildcard refers to the variable being refined.

@Refinement("_ >= 0 && _ <= 100")
int percentage;
percentage = 50;        // Correct
percentage = 10 + 99;   // Error

Class fields can be refined like any local variable. The RGB alias keeps each channel between 0 and 255.

@RefinementAlias("RGB(int x) { x >= 0 && x <= 255 }")
class MyColor {
  @Refinement("RGB(r)") int r;
  @Refinement("RGB(_)") int g;
  @Refinement("RGB(_)") int b;
}

Refine the return type with an annotation above the method. The _ wildcard refers to the return value.

@Refinement("_ >= 0 && _ >= n")
public static int absolute(int n) {
  if (0 <= n)  return n;
  else         return 0 - n;
}

Refine method parameters. Both must satisfy the Percentage alias, and bonus can refer to grade (later parameters can mention earlier ones, never the reverse).

@RefinementAlias("Percentage(int x) { x >= 0 && x <= 100 }")
public class Grade {

  @Refinement("Percentage(_)")
  public static int addBonus(
      @Refinement("Percentage(_)") int grade,
      @Refinement("Percentage(_) && bonus < grade") int bonus) {
    if ((bonus + grade) > 100) return 100;
    else                       return grade + bonus;
  }
}