Random Property Test Finds a Bug
Problem
A function buggyMax is meant to return the biggest number of a list, but it has a bug: its loop stops one element too early, so it never looks at the last element when the list has 3 or more numbers. Write a tiny property test: for case = 1, 2, ..., count generate a list with a simple random generator and check the property buggyMax(list) == real maximum. The generator is x = x * 48271 mod 2147483647 (start with x = seed; each call first updates x and then uses the new x). For every case: the list length is (next x mod 6) + 1, then each element is (next x mod 10). Print the first failing case as case i: followed by the list (numbers separated by spaces), or no counterexample if all cases pass.
Constraints
- 1 <= seed <= 10^6
- 1 <= count <= 10^4
Examples
Input
1 100
Output
case 1: 4 6
Solutions
A property test checks a rule for many generated inputs instead of a few hand-picked ones. When it fails, the failing input is the starting point for debugging. Libraries such as jqwik (Java), fast-check (JavaScript) and Hypothesis (Python) also shrink the failing input to a minimal one. A fixed seed makes the run repeatable.
/*
* Problem : First counterexample.
* Input : seed and count.
* Output : A case line or no counterexample.
* Approach: Generate and check.
* Time : O(count)
* Space : O(1)
* Java : 8 or newer.
*/
import java.util.Scanner;
public class Main {
// Step 1: The function under test. Its loop stops at length - 1, so the last element is never checked.
static int buggyMax(int[] list) {
int best = list[0];
for (int i = 1; i < list.length - 1; i++) {
best = Math.max(best, list[i]);
}
return best;
}
// This method solves the task. It receives the input and returns the answer.
static String solve(long a, long b) {
// Step 2: A small random generator with a fixed rule gives the same lists on every run.
long x = a;
for (long testCase = 1; testCase <= b; testCase++) {
x = x * 48271 % 2147483647L;
int length = (int) (x % 6) + 1;
int[] list = new int[length];
int real = -1;
for (int i = 0; i < length; i++) {
x = x * 48271 % 2147483647L;
list[i] = (int) (x % 10);
real = Math.max(real, list[i]);
}
// Step 3: The property: the function must give the real maximum. The first failure is our counterexample.
if (buggyMax(list) != real) {
StringBuilder text = new StringBuilder("case " + testCase + ":");
for (int value : list) {
text.append(' ').append(value);
}
return text.toString();
}
}
return "no counterexample";
}
public static void main(String[] args) {
Scanner scanner = new Scanner(System.in);
long a = scanner.nextLong();
long b = scanner.nextLong();
System.out.println(solve(a, b));
}
}
Hints (1)
- Why must the seed be fixed in a test suite?