Define property methods as "getters"

docs/manual/purity-checker.tex

@@ -113,7 +113,8 @@
 unsoundly assume that every getter method is side-effect-free and
 deterministic.  For the purposes of \<-AassumePureGetters>, a getter method
 is defined as an instance method with no formal parameters, whose name
-starts with ``get'' followed by an uppercase letter.
+starts with ``get'', ``is'', ``not'', or ``has'' followed by an uppercase
+letter.
 
 This can make
 flow-sensitive type refinement much more effective, since method calls will

javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java

@@ -1101,7 +1101,8 @@ public static boolean isResourceVariable(@Nullable Element elt) {
 
   /**
    * Returns true if the given element is a getter method. A getter method is an instance method
-   * with no formal parameters, whose name starts with "get" followed by an upper-case letter.
+   * with no formal parameters, whose name starts with "get", "is", "not", or "has" followed by an
+   * upper-case letter.
    *
    * @param methodElt a method
    * @return true if the given element is a getter method
@@ -1117,12 +1118,18 @@ public static boolean isGetter(@Nullable ExecutableElement methodElt) {
       return false;
     }
 
-    // I could check that the method has a non-void return type.
+    // I could check that the method has a non-void return type,
+    // and that methods with prefix "is", "has", and "not" return boolean.
 
     // Constructors and initializers don't have a name starting with a character.
     String name = methodElt.getSimpleName().toString();
     // I expect this code is more efficient than use of a regular expression.
-    boolean nameOk = nameStartsWith(name, "get");
+    boolean nameOk =
+        nameStartsWith(name, "get")
+            || nameStartsWith(name, "is")
+            || nameStartsWith(name, "not")
+            || nameStartsWith(name, "has");
+
     if (!nameOk) {
       return false;
     }