Class Effect

java.lang.Object
org.checkerframework.checker.guieffect.Effect
public final class Effect extends Object
An effect -- either UIEffect, PolyUIEffect, or SafeEffect.

  • Constructor Details

    • Effect

      public Effect(Class<? extends Annotation> cls)
      Create a new Effect object.
      Parameters:
      cls - one of UIEffect.class, PolyUIEffect.class, or SafeEffect.class

  • Method Details

    • lessThanOrEqualTo

      public static boolean lessThanOrEqualTo(Effect left, Effect right)
      Return true iff left is less than or equal to right.
      Parameters:
      left - the first effect to compare
      right - the first effect to compare
      Returns:
      true iff left is less than or equal to right

    • min

      public static Effect min(Effect l, Effect r)

    • isSafe

      public boolean isSafe()
      Return true if this is SafeEffect.
      Returns:
      true if this is SafeEffect

    • isUI

      public boolean isUI()
      Return true if this is UIEffect.
      Returns:
      true if this is UIEffect

    • isPoly

      @Pure public boolean isPoly()
      Return true if this is PolyUIEffect.
      Returns:
      true if this is PolyUIEffect

    • getAnnot

      public Class<? extends Annotation> getAnnot()

    • toString

      @SideEffectFree public String toString()
      Overrides:
      toString in class Object

    • equals

      public boolean equals(Effect e)
      Return true if this equals the given effect.
      Parameters:
      e - the effect to compare this to
      Returns:
      true if this equals the given effect

    • equals

      public boolean equals(@Nullable Object o)
      Overrides:
      equals in class Object

    • hashCode

      @Pure public int hashCode()
      Overrides:
      hashCode in class Object