Running JVerify
Let’s try running JVerify on the following Java program, found here:
package org.strata.jverify.examples;
import static org.strata.jverify.JVerify.*;
class GaussianSum {
/**
* Returns 0 + 1 + 2 + ... + n.
*
* JVerify proves that the result equals the closed form n * (n + 1) / 2
* for every n in [0, 65535]. The proof relies on two loop invariants:
* a bound on the loop counter, and a closed-form relation that holds at
* every iteration.
*/
static int sumTo(int n) {
precondition(0 <= n && n <= 65535);
postcondition((int res) -> res == n * (n + 1) / 2);
int i = 0;
int s = 0;
while (i < n) {
invariant(0 <= i && i <= n);
invariant(s == i * (i + 1) / 2);
i = i + 1;
s = s + i;
}
return s;
}
}
sumTo(n) claims it returns the closed form n * (n + 1) / 2. JVerify checks that claim against the actual loop using two invariants: one bounds the loop counter, the other ties the running sum to the closed form.
To run JVerify, from the repository root:
./verifier/build/install/verifier/bin/verifier ./examples/src/test/java/org/strata/jverify/examples/GaussianSum.java
or on Windows:
./verifier/build/install/verifier/bin/verifier.bat ./examples/src/test/java/org/strata/jverify/examples/GaussianSum.java
You should see the following output:
Found 0 errors
Verified methods: 2
Failed methods: 0
Skipped methods: 0
If the JVERIFY_STRATA environment variable is not set, pass the Strata project directory explicitly with --strata ./Strata.
Try editing GaussianSum.java to introduce a bug — for example, change return s; to return s + 1; — and re-run. JVerify reports:
GaussianSum.java(16:36-16:58): Error: assertion could not be proved
Found 1 errors
Verified methods: 1
Failed methods: 1
Skipped methods: 0
The line and column point at the failing postcondition.
Adding JVerify to a Java project
To verify your own code, add the JVerify library as a compile-time dependency so you can use annotations such as @Pure and specification methods such as precondition. In a Gradle build script:
dependencies {
implementation("org.strata.jverify:library:1.0-SNAPSHOT")
// ...
}
Because the JVerify packages are not yet published to any shared repositories, run ./gradlew publishToMavenLocal first so this can be resolved. See the sample project for more details.
Current limitations
JVerify currently supports a limited subset of Java. See Supported Java features and issue #384 for the current state.