Quickcheck (#663)

* quickcheck/property tests for IntCharSet includes generator for IntCharSet; addresses #662 * add junit-quickcheck bazel dependencies * add junit-quickcheck pom dependencies * IntCharSet: add debug assertions on add/sub Sort-of obvious, but would be nasty if violated. Discovered in quickcheck property testing.
jflex-de · Dec 8, 2019 · 6835dda · 6835dda
1 parent fd2ece2
commit 6835dda
Show file tree

Hide file tree

Showing 10 changed files with 469 additions and 5 deletions.
diff --git a/WORKSPACE b/WORKSPACE
@@ -64,10 +64,6 @@ maven_install(
     ],
 )
 
-# To update maven_install.json, run this command to re-pin the unpinned repository:
-#
-#    bazel run @unpinned_maven//:pin
-#
 load("@maven//:defs.bzl", "pinned_maven_install")
 
 pinned_maven_install()

diff --git a/jflex/pom.xml b/jflex/pom.xml
@@ -81,6 +81,24 @@
       <artifactId>truth</artifactId>
       <scope>test</scope>
     </dependency>
+    <dependency>
+      <groupId>com.pholser</groupId>
+      <artifactId>junit-quickcheck-core</artifactId>
+      <version>0.9</version>
+      <scope>test</scope>
+    </dependency>
+    <dependency>
+      <groupId>com.pholser</groupId>
+      <artifactId>junit-quickcheck-generators</artifactId>
+      <version>0.9</version>
+      <scope>test</scope>
+    </dependency>
+    <dependency>
+      <groupId>org.slf4j</groupId>
+      <artifactId>slf4j-simple</artifactId>
+      <version>1.7.28</version>
+      <scope>test</scope>
+    </dependency>
   </dependencies>
   <build>
     <plugins>
@@ -91,6 +109,7 @@
           <includes>
             <include>**/*Test.java</include>
             <include>**/*Tests.java</include>
+            <include>**/*Quickcheck.java</include>
           </includes>
         </configuration>
       </plugin>

diff --git a/jflex/src/main/java/jflex/core/IntCharSet.java b/jflex/src/main/java/jflex/core/IntCharSet.java
@@ -138,6 +138,11 @@ private int indexOf(int c) {
 
   /** Merges the given set into this one. */
   public void add(IntCharSet set) {
+    if (DEBUG) {
+      assert invariants();
+      assert set.invariants();
+      assert this != set;
+    }
     for (Interval interval : set.intervals) {
       add(interval);
     }
@@ -372,6 +377,7 @@ public void sub(IntCharSet set) {
       // not asserting non-null, because we'll already get an exception and it confuses lgtm.com
       assert set.invariants();
       assert isSubSet(set, this);
+      assert set != this;
     }
 
     int i = 0; // index in this.intervals

diff --git a/jflex/src/test/java/jflex/core/BUILD b/jflex/src/test/java/jflex/core/BUILD
@@ -8,6 +8,20 @@ java_test(
     ],
 )
 
+java_test(
+    name = "IntCharSetQuickcheck",
+    srcs = [
+        "IntCharSetGen.java",
+        "IntCharSetQuickcheck.java",
+    ],
+    deps = [
+        "//jflex/src/main/java/jflex/chars",
+        "//jflex/src/main/java/jflex/core",
+        "//third_party/com/google/truth",
+        "//third_party/com/pholser/quickcheck",
+    ],
+)
+
 java_test(
     name = "IntCharSetTest",
     srcs = ["IntCharSetTest.java"],

diff --git a/jflex/src/test/java/jflex/core/IntCharSetGen.java b/jflex/src/test/java/jflex/core/IntCharSetGen.java
@@ -0,0 +1,89 @@
+/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
+ * JFlex 1.8.0-SNAPSHOT                                                    *
+ * Copyright (C) 1998-2019  Gerwin Klein <lsf@jflex.de>                    *
+ * All rights reserved.                                                    *
+ *                                                                         *
+ * License: BSD                                                            *
+ *                                                                         *
+ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
+
+package jflex.core;
+
+import com.pholser.junit.quickcheck.generator.GenerationStatus;
+import com.pholser.junit.quickcheck.generator.Generator;
+import com.pholser.junit.quickcheck.generator.InRange;
+import com.pholser.junit.quickcheck.generator.Size;
+import com.pholser.junit.quickcheck.random.SourceOfRandomness;
+import jflex.chars.Interval;
+
+/**
+ * Generator for random {@link IntCharSet} instances.
+ *
+ * @author Gerwin Klein
+ * @version JFlex 1.8.0-SNAPSHOT
+ * @see IntCharSet
+ */
+public class IntCharSetGen extends Generator<IntCharSet> {
+
+  /** Min bound for intervals */
+  private int minChar = 0;
+  /** Max bound for intervals. Small for speed, and more likely edge cases. */
+  private int maxChar = 50;
+
+  /** Min bound for number of intervals (0 = empty set) */
+  private int minSize = 0;
+  /** Max bound for number of intervals */
+  private int maxSize = 5;
+
+  /** Constructs generator for IntCharSet */
+  public IntCharSetGen() {
+    super(IntCharSet.class);
+  }
+
+  @Override
+  public IntCharSet generate(SourceOfRandomness r, GenerationStatus status) {
+    IntCharSet result = new IntCharSet();
+
+    int numIntervals = r.nextInt(minSize, maxSize);
+    for (int i = 0; i < numIntervals; i++) {
+      int start = r.nextInt(minChar, maxChar);
+      int end = r.nextInt(start, maxChar);
+
+      // pick default with higher probability
+      switch (r.nextInt(0, 4)) {
+        case 0:
+          result.add(IntCharSet.ofCharacter(start));
+          break;
+        case 1:
+          result.add(start);
+          break;
+        default:
+          result.add(new Interval(start, end));
+          break;
+      }
+    }
+
+    return result;
+  }
+
+  /**
+   * Configure this generator to only produce intervals in the given range.
+   *
+   * @param range annotation that contains the intervals constraints
+   */
+  public void configure(InRange range) {
+    minChar = Math.max(0, range.minInt());
+    maxChar = Math.min(range.maxInt(), CharClasses.maxChar);
+  }
+
+  /**
+   * Configure this generator to only produce IntCharSets with a given range of number of intervals.
+   *
+   * @param size annotation that contains how many intervals the IntCharSet should contain at least
+   *     and at most
+   */
+  public void configure(Size size) {
+    minSize = size.min();
+    maxSize = size.max();
+  }
+}
diff --git a/jflex/src/test/java/jflex/core/IntCharSetQuickcheck.java b/jflex/src/test/java/jflex/core/IntCharSetQuickcheck.java
@@ -0,0 +1,171 @@
+/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
+ * JFlex 1.8.0-SNAPSHOT                                                    *
+ * Copyright (C) 1998-2019  Gerwin Klein <lsf@jflex.de>                    *
+ * All rights reserved.                                                    *
+ *                                                                         *
+ * License: BSD                                                            *
+ *                                                                         *
+ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
+
+package jflex.core;
+
+import static com.google.common.truth.Truth.assertThat;
+
+import com.pholser.junit.quickcheck.Property;
+import com.pholser.junit.quickcheck.generator.InRange;
+import com.pholser.junit.quickcheck.runner.JUnitQuickcheck;
+import org.junit.runner.RunWith;
+
+/**
+ * Property-based tests for {@link IntCharSet}
+ *
+ * @author Gerwin Klein
+ * @version JFlex 1.8.0-SNAPSHOT
+ * @see IntCharSet
+ */
+@RunWith(JUnitQuickcheck.class)
+public class IntCharSetQuickcheck {
+
+  @Property
+  public void addIsUnion(IntCharSet s1, IntCharSet s2) {
+    IntCharSet union = IntCharSet.copyOf(s1);
+    union.add(s2);
+
+    assertThat(union.invariants()).isTrue();
+
+    assertThat(IntCharSet.isSubSet(s1, union)).isTrue();
+    assertThat(IntCharSet.isSubSet(s2, union)).isTrue();
+
+    for (int i : union) {
+      assertThat(s1.contains(i) || s2.contains(i)).isTrue();
+    }
+  }
+
+  @Property
+  public void andIsIntersection(
+      @InRange(maxInt = 100) IntCharSet s1, @InRange(maxInt = 100) IntCharSet s2) {
+    IntCharSet inter = s1.and(s2);
+
+    assertThat(inter.invariants()).isTrue();
+
+    assertThat(IntCharSet.isSubSet(inter, s1)).isTrue();
+    assertThat(IntCharSet.isSubSet(inter, s2)).isTrue();
+
+    for (int i : s1) {
+      assertThat(!s2.contains(i) || inter.contains(i)).isTrue();
+    }
+  }
+
+  @Property
+  public void andCommutes(IntCharSet s1, IntCharSet s2) {
+    assertThat(s1.and(s2)).isEqualTo(s2.and(s1));
+  }
+
+  @Property
+  public void addSelf(IntCharSet set) {
+    IntCharSet setPre = IntCharSet.copyOf(set);
+    set.add(setPre);
+    assertThat(set).isEqualTo(setPre);
+  }
+
+  @Property
+  public void addIdemPotent(IntCharSet s1, IntCharSet s2) {
+    IntCharSet union1 = IntCharSet.copyOf(s1);
+    union1.add(s2);
+    IntCharSet union2 = IntCharSet.copyOf(union1);
+    union2.add(s2);
+    assertThat(union2).isEqualTo(union1);
+  }
+
+  @Property
+  public void subIsDifference(IntCharSet s1, IntCharSet s2) {
+    IntCharSet diff = IntCharSet.copyOf(s1);
+    // use intersection to ensure that argument of sub is contained in s1
+    diff.sub(s1.and(s2));
+
+    assertThat(diff.invariants()).isTrue();
+
+    assertThat(IntCharSet.isSubSet(diff, s1)).isTrue();
+    assertThat(diff.and(s2).containsElements()).isFalse();
+
+    // union of the diff and s2 should be equal to union of s1 and s2
+    diff.add(s2);
+    IntCharSet s3 = IntCharSet.copyOf(s1);
+    s3.add(s2);
+    assertThat(diff).isEqualTo(s3);
+  }
+
+  @Property
+  public void containsItsElements(IntCharSet set) {
+    for (int i : set) assertThat(set.contains(i)).isTrue();
+  }
+
+  @Property
+  public void allCharsContainsEverything(IntCharSet set) {
+    assertThat(IntCharSet.allChars().contains(set)).isTrue();
+  }
+
+  @Property
+  public void addSubEq(IntCharSet s1, IntCharSet s2) {
+    IntCharSet s1Pre = IntCharSet.copyOf(s1);
+    IntCharSet inter = s1.and(s2);
+
+    s1.sub(inter);
+    s1.add(inter);
+
+    assertThat(s1).isEqualTo(s1Pre);
+  }
+
+  @Property
+  public void addEmpty(IntCharSet set) {
+    IntCharSet setPre = IntCharSet.copyOf(set);
+    set.add(new IntCharSet());
+    assertThat(set).isEqualTo(setPre);
+  }
+
+  @Property
+  public void subEmpty(IntCharSet set) {
+    IntCharSet setPre = IntCharSet.copyOf(set);
+    set.sub(new IntCharSet());
+    assertThat(set).isEqualTo(setPre);
+  }
+
+  @Property
+  public void andEmpty(IntCharSet set) {
+    assertThat(set.and(new IntCharSet())).isEqualTo(new IntCharSet());
+  }
+
+  @Property
+  public void addAll(IntCharSet set) {
+    set.add(IntCharSet.allChars());
+    assertThat(set).isEqualTo(IntCharSet.allChars());
+  }
+
+  @Property
+  public void subSelf(IntCharSet set) {
+    set.sub(IntCharSet.copyOf(set));
+    assertThat(set).isEqualTo(new IntCharSet());
+  }
+
+  @Property
+  public void andAll(IntCharSet set) {
+    assertThat(set.and(IntCharSet.allChars())).isEqualTo(set);
+  }
+
+  @Property
+  public void andSelf(IntCharSet set) {
+    assertThat(set.and(set)).isEqualTo(set);
+  }
+
+  @Property
+  public void complement(IntCharSet set) {
+    IntCharSet comp = IntCharSet.allChars();
+    comp.sub(set);
+
+    assertThat(comp.invariants()).isTrue();
+    assertThat(comp.and(set).containsElements()).isFalse();
+
+    comp.add(set);
+    assertThat(comp).isEqualTo(IntCharSet.allChars());
+  }
+}
diff --git a/third_party/com/google/auto_value/BUILD b/third_party/com/google/auto_value/BUILD
@@ -1,3 +1,5 @@
+# Google AutoValue
+
 package(default_visibility = ["//visibility:public"])
 
 licenses(["notice"])  # Apache License 2.0

diff --git a/third_party/com/pholser/quickcheck/BUILD b/third_party/com/pholser/quickcheck/BUILD
@@ -0,0 +1,17 @@
+# junit-quickcheck
+# junit-quickcheck is a library that supports writing and running property-based tests in JUnit,
+# inspired by QuickCheck for Haskell.
+# https://github.com/pholser/junit-quickcheck
+
+package(default_visibility = ["//visibility:public"])
+
+licenses(["notice"])  # MIT License
+
+java_library(
+    name = "quickcheck",
+    testonly = True,
+    exports = [
+        "@maven//:com_pholser_junit_quickcheck_core",
+        "@maven//:com_pholser_junit_quickcheck_generators",
+    ],
+)
diff --git a/third_party/deps.bzl b/third_party/deps.bzl
@@ -1,4 +1,8 @@
 # Please keep deps in alphabetical order
+# After a change in deps, run this command to re-pin the unpinned repository:
+#
+#    bazel run @unpinned_maven//:pin
+#
 ARTIFACTS = [
     "com.google.code.findbugs:jsr305:3.0.2",
     "org.apache.ant:ant:1.7.0",
@@ -11,5 +15,7 @@ ARTIFACTS = [
     "com.google.flogger:flogger-system-backend:0.4",
     "com.google.guava:guava:jar:26.0-jre",
     "com.google.truth:truth:0.36",
+    "com.pholser:junit-quickcheck-core:0.9",
+    "com.pholser:junit-quickcheck-generators:0.9",
     "junit:junit:jar:4.12",
 ]