From 12661d9dfaec2599b7b739234a4824d6bb4036ed Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 18:53:26 +0100 Subject: [PATCH] Add comprehensive Java modeling constructs documentation - Create new java-modeling-constructs.md with detailed guide - Document assertions, non-determinism, and assumptions in Java - Add practical examples and code samples - Integrate documentation into manual index - Reference in JBMC user manual Fixes: #611 --- .../examples/AssertionExamples.java | 88 +++ .../examples/AssumptionExamples.java | 232 +++++++ .../examples/BankingExample.java | 86 +++ .../examples/NondeterminismExamples.java | 178 ++++++ doc/cprover-manual/examples/QuickReference.md | 306 ++++++++++ doc/cprover-manual/examples/README.md | 145 +++++ .../examples/org/cprover/CProver.java | 204 +++++++ .../examples/test-compilation.sh | 42 ++ doc/cprover-manual/index.md | 11 +- .../java-modeling-constructs.md | 565 ++++++++++++++++++ doc/cprover-manual/jbmc-user-manual.md | 8 + 11 files changed, 1862 insertions(+), 3 deletions(-) create mode 100644 doc/cprover-manual/examples/AssertionExamples.java create mode 100644 doc/cprover-manual/examples/AssumptionExamples.java create mode 100644 doc/cprover-manual/examples/BankingExample.java create mode 100644 doc/cprover-manual/examples/NondeterminismExamples.java create mode 100644 doc/cprover-manual/examples/QuickReference.md create mode 100644 doc/cprover-manual/examples/README.md create mode 100644 doc/cprover-manual/examples/org/cprover/CProver.java create mode 100755 doc/cprover-manual/examples/test-compilation.sh create mode 100644 doc/cprover-manual/java-modeling-constructs.md diff --git a/doc/cprover-manual/examples/AssertionExamples.java b/doc/cprover-manual/examples/AssertionExamples.java new file mode 100644 index 00000000000..37f9298394c --- /dev/null +++ b/doc/cprover-manual/examples/AssertionExamples.java @@ -0,0 +1,88 @@ +import org.cprover.CProver; + +/** + * Examples demonstrating various assertion patterns in JBMC + */ +public class AssertionExamples { + + /** + * Example 1: Basic assertion + */ + public static void basicAssertion(int x) { + assert x > 0 : "x must be positive"; + } + + /** + * Example 2: Array bounds safety + */ + public static void arrayBoundsSafety(int[] arr, int index) { + // Explicitly assert bounds (JBMC also checks this automatically) + assert arr != null : "array must not be null"; + assert index >= 0 && index < arr.length : "index must be within bounds"; + + int value = arr[index]; + assert value >= 0 : "array contains non-negative values"; + } + + /** + * Example 3: Verifying mathematical properties + */ + public static void mathematicalProperties() { + int a = CProver.nondetInt(); + int b = CProver.nondetInt(); + + // Constrain inputs to prevent overflow + CProver.assume(a >= -1000 && a <= 1000); + CProver.assume(b >= -1000 && b <= 1000); + + // Verify commutativity of addition + assert a + b == b + a : "addition is commutative"; + + // Verify associativity (when no overflow occurs) + int c = CProver.nondetInt(); + CProver.assume(c >= -1000 && c <= 1000); + assert (a + b) + c == a + (b + c) : "addition is associative"; + } + + /** + * Example 4: Verifying all array elements + */ + public static void verifyAllElements(int[] arr) { + CProver.assume(arr != null); + CProver.assume(arr.length > 0 && arr.length <= 10); + + // Initialize all elements to zero + for (int i = 0; i < arr.length; i++) { + arr[i] = 0; + } + + // Use non-determinism to check all elements + int index = CProver.nondetInt(); + CProver.assume(index >= 0 && index < arr.length); + + // This assertion checks that ALL elements are zero + assert arr[index] == 0 : "all array elements are zero"; + } + + /** + * Example 5: Pre and postconditions + */ + public static int divide(int numerator, int denominator) { + // Precondition + assert denominator != 0 : "denominator must not be zero"; + + int result = numerator / denominator; + + // Postcondition + assert result * denominator <= numerator || + result * denominator >= numerator : + "result is consistent with division"; + + return result; + } + + public static void main(String[] args) { + // These would be run by JBMC + mathematicalProperties(); + } +} diff --git a/doc/cprover-manual/examples/AssumptionExamples.java b/doc/cprover-manual/examples/AssumptionExamples.java new file mode 100644 index 00000000000..a212e151940 --- /dev/null +++ b/doc/cprover-manual/examples/AssumptionExamples.java @@ -0,0 +1,232 @@ +import org.cprover.CProver; + +/** + * Examples demonstrating the use of assumptions in JBMC + */ +public class AssumptionExamples { + + /** + * Example 1: Basic assumption usage + */ + public static void basicAssumption() { + int x = CProver.nondetInt(); + + // Restrict x to be in the range [1, 100] + CProver.assume(x >= 1 && x <= 100); + + // Now JBMC will only consider values where 1 <= x <= 100 + assert x > 0 : "x is positive"; // This will succeed + assert x <= 100 : "x is at most 100"; // This will succeed + } + + /** + * Example 2: Contrasting assumptions with assertions + */ + public static void assumptionVsAssertion() { + // INCORRECT approach - using assertion to constrain + int x1 = CProver.nondetInt(); + // assert x1 > 0; // This would FAIL because x1 can be negative + + // CORRECT approach - using assumption to constrain + int x2 = CProver.nondetInt(); + CProver.assume(x2 > 0); // Only consider positive x2 + assert x2 > 0; // This SUCCEEDS because x2 is constrained + } + + /** + * Example 3: Assumption ordering matters + */ + public static void assumptionOrdering() { + // WRONG: Assertion before assumption + int x = CProver.nondetInt(); + // assert x == 100; // This would fail + // CProver.assume(x == 100); // Too late! + + // CORRECT: Assumption before assertion + int y = CProver.nondetInt(); + CProver.assume(y == 100); // Constrain first + assert y == 100; // This succeeds + } + + /** + * Example 4: Constrained array access + */ + public static void safeArrayAccess(int[] arr) { + // Assume preconditions + CProver.assume(arr != null); + CProver.assume(arr.length > 0); + + int index = CProver.nondetInt(); + // Constrain index to valid range + CProver.assume(index >= 0 && index < arr.length); + + // This access is now guaranteed to be safe + int value = arr[index]; + assert value == arr[index]; // Trivially true, but demonstrates safety + } + + /** + * Example 5: Multiple constraints + */ + public static void multipleConstraints() { + int a = CProver.nondetInt(); + int b = CProver.nondetInt(); + + // Apply multiple constraints + CProver.assume(a >= 0); // a is non-negative + CProver.assume(b >= 0); // b is non-negative + CProver.assume(a <= 1000); // a is bounded above + CProver.assume(b <= 1000); // b is bounded above + CProver.assume(a != b); // a and b are different + + // Now verify properties under these constraints + assert a >= 0 && b >= 0 : "both values are non-negative"; + assert a != b : "values are different"; + } + + /** + * Example 6: Modeling preconditions + */ + public static int safeDivide(int numerator, int denominator) { + return numerator / denominator; + } + + public static void testSafeDivide() { + int num = CProver.nondetInt(); + int den = CProver.nondetInt(); + + // Model the precondition as an assumption + CProver.assume(den != 0); // Division by zero not allowed + + // Also prevent overflow + CProver.assume(num >= -1000000 && num <= 1000000); + CProver.assume(den >= -1000000 && den <= 1000000); + + int result = safeDivide(num, den); + + // Verify properties + if (num == 0) { + assert result == 0 : "zero divided by anything is zero"; + } + if (den == 1) { + assert result == num : "dividing by 1 gives original number"; + } + } + + /** + * Example 7: Modeling object properties + */ + public static class Rectangle { + int width, height; + + public Rectangle(int w, int h) { + this.width = w; + this.height = h; + } + + public int area() { + return width * height; + } + } + + public static void verifyRectangleArea() { + int w = CProver.nondetInt(); + int h = CProver.nondetInt(); + + // Assume valid dimensions + CProver.assume(w > 0 && w <= 1000); + CProver.assume(h > 0 && h <= 1000); + + Rectangle rect = new Rectangle(w, h); + int area = rect.area(); + + // Verify properties + assert area > 0 : "area of valid rectangle is positive"; + assert area == w * h : "area calculation is correct"; + assert area >= w : "area is at least width"; + assert area >= h : "area is at least height"; + } + + /** + * Example 8: Warning - Unsatisfiable assumptions + */ + public static void unsatisfiableAssumptions() { + int x = CProver.nondetInt(); + + // These assumptions are contradictory! + CProver.assume(x > 100); + CProver.assume(x < 50); + + // This will "succeed" but vacuously - there are no valid inputs + // assert false; // Would incorrectly pass! + + // Better: Use satisfiable assumptions + int y = CProver.nondetInt(); + CProver.assume(y > 50 && y < 100); + assert y > 50 && y < 100; // Meaningful verification + } + + /** + * Example 9: Bounded input helpers + */ + + // Helper: Generate percentage (0-100) + public static int nondetPercentage() { + int percentage = CProver.nondetInt(); + CProver.assume(percentage >= 0 && percentage <= 100); + return percentage; + } + + // Helper: Generate positive integer + public static int nondetPositive() { + int value = CProver.nondetInt(); + CProver.assume(value > 0); + return value; + } + + public static void testBoundedHelpers() { + int pct = nondetPercentage(); + assert pct >= 0 && pct <= 100 : "percentage is in valid range"; + + int pos = nondetPositive(); + assert pos > 0 : "positive value is positive"; + } + + /** + * Example 10: Complex constraints + */ + public static void complexConstraints() { + int[] arr = CProver.nondetWithoutNull(); + + // Constrain array properties + CProver.assume(arr.length >= 2 && arr.length <= 10); + + // Constrain array contents + for (int i = 0; i < arr.length; i++) { + CProver.assume(arr[i] >= 0 && arr[i] <= 100); + } + + // Additional constraint: array is sorted + for (int i = 1; i < arr.length; i++) { + CProver.assume(arr[i] >= arr[i-1]); + } + + // Now verify properties of sorted array + assert arr[0] <= arr[arr.length - 1] : "first element <= last element"; + + // Check any two adjacent elements + int index = CProver.nondetInt(); + CProver.assume(index >= 0 && index < arr.length - 1); + assert arr[index] <= arr[index + 1] : "array is sorted"; + } + + public static void main(String[] args) { + // Run examples + basicAssumption(); + assumptionVsAssertion(); + testSafeDivide(); + verifyRectangleArea(); + testBoundedHelpers(); + complexConstraints(); + } +} \ No newline at end of file diff --git a/doc/cprover-manual/examples/BankingExample.java b/doc/cprover-manual/examples/BankingExample.java new file mode 100644 index 00000000000..73f67d6e9d7 --- /dev/null +++ b/doc/cprover-manual/examples/BankingExample.java @@ -0,0 +1,86 @@ +import org.cprover.CProver; + +/** + * Example: Verifying a simple banking operation + * + * This example demonstrates the use of assertions, non-determinism, + * and assumptions in JBMC verification. + */ +public class BankingExample { + + /** + * Transfer money from one account to another + * @param fromBalance - source account balance + * @param toBalance - destination account balance + * @param amount - amount to transfer + * @return true if transfer succeeded, false otherwise + */ + public static boolean transfer(int fromBalance, int toBalance, int amount) { + if (amount <= 0) { + return false; // Invalid amount + } + if (fromBalance < amount) { + return false; // Insufficient funds + } + // Transfer successful + return true; + } + + /** + * Verification harness for the transfer function + */ + public static void verifyTransfer() { + // 1. NON-DETERMINISM: Create arbitrary inputs + int fromBalance = CProver.nondetInt(); + int toBalance = CProver.nondetInt(); + int amount = CProver.nondetInt(); + + // 2. ASSUMPTIONS: Constrain inputs to valid ranges + // Balances must be non-negative + CProver.assume(fromBalance >= 0); + CProver.assume(toBalance >= 0); + // Amount must be reasonable (prevent overflow) + CProver.assume(amount >= 0 && amount <= 1000000); + + // Call the function under test + boolean result = transfer(fromBalance, toBalance, amount); + + // 3. ASSERTIONS: Verify expected properties + + // Property 1: Transfer fails for non-positive amounts + if (amount <= 0) { + assert !result : "transfer should fail for non-positive amount"; + } + + // Property 2: Transfer fails for insufficient funds + if (amount > 0 && fromBalance < amount) { + assert !result : "transfer should fail for insufficient funds"; + } + + // Property 3: Transfer succeeds when conditions are met + if (amount > 0 && fromBalance >= amount) { + assert result : "transfer should succeed when funds are sufficient"; + } + } + + /** + * Example with object non-determinism + */ + public static void verifyWithObjects() { + // Create non-deterministic String that might be null + String message = CProver.nondetWithNull(); + + // Assume it's non-null for this test + CProver.assume(message != null); + + // Now we can safely use the string + int length = message.length(); + assert length >= 0 : "string length is non-negative"; + } + + public static void main(String[] args) { + // Run verification harnesses + verifyTransfer(); + verifyWithObjects(); + } +} diff --git a/doc/cprover-manual/examples/NondeterminismExamples.java b/doc/cprover-manual/examples/NondeterminismExamples.java new file mode 100644 index 00000000000..8a26ad54d2d --- /dev/null +++ b/doc/cprover-manual/examples/NondeterminismExamples.java @@ -0,0 +1,178 @@ +import org.cprover.CProver; + +/** + * Examples demonstrating non-determinism in JBMC + */ +public class NondeterminismExamples { + + /** + * Example 1: All primitive type non-deterministic values + */ + public static void allPrimitiveTypes() { + // Generate non-deterministic primitive values + boolean b = CProver.nondetBoolean(); // arbitrary boolean + byte by = CProver.nondetByte(); // arbitrary byte + char c = CProver.nondetChar(); // arbitrary char + short s = CProver.nondetShort(); // arbitrary short + int i = CProver.nondetInt(); // arbitrary int + long l = CProver.nondetLong(); // arbitrary long + float f = CProver.nondetFloat(); // arbitrary float + double d = CProver.nondetDouble(); // arbitrary double + + // These values can be anything within their type's range + System.out.println("Non-deterministic values generated"); + } + + /** + * Example 2: Non-deterministic object with null + */ + public static void nondetWithNull() { + // This string might be null or a valid String + String s = CProver.nondetWithNull(); + + if (s != null) { + int length = s.length(); + assert length >= 0 : "string length is non-negative"; + } else { + // Handle the null case + System.out.println("String is null"); + } + } + + /** + * Example 3: Non-deterministic object without null + */ + public static void nondetWithoutNull() { + // This string is guaranteed to be non-null + String s = CProver.nondetWithoutNull(); + + // No null check needed! + int length = s.length(); + assert length >= 0 : "string length is non-negative"; + } + + /** + * Example 4: Verifying a function with arbitrary inputs + */ + public static int absolute(int x) { + if (x < 0) { + return -x; + } + return x; + } + + public static void verifyAbsolute() { + // Test with arbitrary input + int x = CProver.nondetInt(); + + // Constrain to prevent overflow + CProver.assume(x != Integer.MIN_VALUE); + + int result = absolute(x); + + // Verify the result is always non-negative + assert result >= 0 : "absolute value is non-negative"; + + // Verify the result has correct magnitude + if (x >= 0) { + assert result == x : "absolute of positive is itself"; + } else { + assert result == -x : "absolute of negative is negation"; + } + } + + /** + * Example 5: Using non-determinism to find edge cases + */ + public static boolean isPrime(int n) { + if (n <= 1) return false; + if (n == 2) return true; + if (n % 2 == 0) return false; + + for (int i = 3; i * i <= n; i += 2) { + if (n % i == 0) return false; + } + return true; + } + + public static void testPrimeCounter() { + int n = CProver.nondetInt(); + + // Only test in a reasonable range + CProver.assume(n >= 1 && n <= 100); + + boolean result = isPrime(n); + + // Verify known primes + if (n == 2 || n == 3 || n == 5 || n == 7) { + assert result : "small primes are correctly identified"; + } + + // Verify known composites + if (n == 4 || n == 6 || n == 8 || n == 9) { + assert !result : "small composites are correctly identified"; + } + } + + /** + * Example 6: Modeling input with specific characteristics + */ + public static class Person { + String name; + int age; + + public Person(String name, int age) { + this.name = name; + this.age = age; + } + } + + public static boolean isAdult(Person p) { + return p.age >= 18; + } + + public static void verifyIsAdult() { + // Create a person with non-deterministic age + int age = CProver.nondetInt(); + CProver.assume(age >= 0 && age <= 150); // Reasonable age range + + String name = CProver.nondetWithoutNull(); + Person p = new Person(name, age); + + boolean result = isAdult(p); + + // Verify the classification + if (age >= 18) { + assert result : "person aged 18+ is an adult"; + } else { + assert !result : "person under 18 is not an adult"; + } + } + + /** + * Example 7: Finding counterexamples + */ + public static void findCounterexample() { + int x = CProver.nondetInt(); + int y = CProver.nondetInt(); + + // Constrain to small values + CProver.assume(x >= 0 && x <= 10); + CProver.assume(y >= 0 && y <= 10); + + // This assertion is false - JBMC will find a counterexample + // (try running to see what values it finds!) + // assert x + y != 10 : "sum is never 10"; + + // This assertion is true + assert x + y >= 0 : "sum is non-negative"; + } + + public static void main(String[] args) { + // Run verifications + verifyAbsolute(); + testPrimeCounter(); + verifyIsAdult(); + findCounterexample(); + } +} diff --git a/doc/cprover-manual/examples/QuickReference.md b/doc/cprover-manual/examples/QuickReference.md new file mode 100644 index 00000000000..e5bfa69cbb3 --- /dev/null +++ b/doc/cprover-manual/examples/QuickReference.md @@ -0,0 +1,306 @@ +# JBMC Java Modeling Constructs - Quick Reference + +This is a quick reference guide for using fundamental modeling constructs in +JBMC. For detailed explanations and examples, see the +[full documentation](../java-modeling-constructs.md). + +## Import Statement + +```java +import org.cprover.CProver; +``` + +--- + +## Assertions + +### Standard Java Assertions + +```java +assert condition : "optional message"; +``` + +**Example:** +```java +assert x > 0 : "x must be positive"; +assert arr.length > 0 : "array must not be empty"; +``` + +**Purpose:** Specify properties that JBMC should verify hold for all inputs. + +--- + +## Non-deterministic Values + +### Primitive Types + +| Method | Returns | Description | +|--------|---------|-------------| +| `CProver.nondetBoolean()` | `boolean` | Arbitrary boolean value | +| `CProver.nondetByte()` | `byte` | Arbitrary byte value | +| `CProver.nondetChar()` | `char` | Arbitrary char value | +| `CProver.nondetShort()` | `short` | Arbitrary short value | +| `CProver.nondetInt()` | `int` | Arbitrary int value | +| `CProver.nondetLong()` | `long` | Arbitrary long value | +| `CProver.nondetFloat()` | `float` | Arbitrary float value | +| `CProver.nondetDouble()` | `double` | Arbitrary double value | + +**Example:** +```java +int x = CProver.nondetInt(); // x can be any integer +boolean b = CProver.nondetBoolean(); // b can be true or false +``` + +### Object Types + +| Method | Returns | Null Possible? | +|--------|---------|----------------| +| `CProver.nondetWithNull()` | `` | Yes - may be null | +| `CProver.nondetWithoutNull()` | `` | No - never null | + +**Example:** +```java +String s1 = CProver.nondetWithNull(); // might be null +String s2 = CProver.nondetWithoutNull(); // guaranteed non-null +``` + +**Purpose:** Model arbitrary/unknown input values for exhaustive verification. + +--- + +## Assumptions + +### Basic Usage + +```java +CProver.assume(condition); +``` + +**Purpose:** Constrain the search space by restricting which inputs to consider. + +### Common Patterns + +**Range constraint:** +```java +int x = CProver.nondetInt(); +CProver.assume(x >= 0 && x <= 100); // Only consider 0 <= x <= 100 +``` + +**Non-null constraint:** +```java +String s = CProver.nondetWithNull(); +CProver.assume(s != null); // Only consider non-null strings +``` + +**Array constraints:** +```java +int[] arr = CProver.nondetWithNull(); +CProver.assume(arr != null); +CProver.assume(arr.length > 0 && arr.length <= 10); +``` + +**Multiple constraints:** +```java +int a = CProver.nondetInt(); +int b = CProver.nondetInt(); +CProver.assume(a > 0); +CProver.assume(b > 0); +CProver.assume(a < b); // a is positive and less than b +``` + +--- + +## Key Differences + +### Assertion vs. Assumption + +| Aspect | Assertion (`assert`) | Assumption (`CProver.assume()`) | +|--------|---------------------|--------------------------------| +| **Purpose** | Check a property | Constrain inputs | +| **When false** | Verification FAILS | Input is ignored | +| **Use for** | What you want to PROVE | What you want to ASSUME | + +**Example:** +```java +// WRONG: Using assert to constrain +int x = CProver.nondetInt(); +assert x > 0; // FAILS! x can be <= 0 + +// CORRECT: Use assume to constrain, assert to verify +int x = CProver.nondetInt(); +CProver.assume(x > 0); // Constrain to positive +assert x > 0; // SUCCEEDS - x is positive +``` + +--- + +## Complete Verification Harness Pattern + +```java +import org.cprover.CProver; + +public class MyVerification { + + // Function to verify + public static boolean myFunction(int input) { + if (input < 0) return false; + // ... more logic ... + return true; + } + + // Verification harness + public static void verifyMyFunction() { + // 1. Generate non-deterministic input + int input = CProver.nondetInt(); + + // 2. Constrain input to relevant range + CProver.assume(input >= -1000 && input <= 1000); + + // 3. Call function + boolean result = myFunction(input); + + // 4. Assert expected properties + if (input < 0) { + assert !result : "negative input returns false"; + } else { + // assert other properties... + } + } +} +``` + +--- + +## Running JBMC + +### Basic Command + +```bash +jbmc MyClass --function MyClass.verifyMethod +``` + +### Common Options + +```bash +# Show trace on failure +jbmc MyClass --function MyClass.verify --trace + +# Set loop unwind bound +jbmc MyClass --function MyClass.verify --unwind 10 + +# Enable runtime exceptions +jbmc MyClass --function MyClass.verify --throw-runtime-exceptions + +# Multiple options +jbmc MyClass \ + --function MyClass.verify \ + --unwind 20 \ + --trace \ + --throw-runtime-exceptions +``` + +--- + +## Helper Functions Pattern + +Create helper functions for common input patterns: + +```java +// Generate percentage (0-100) +public static int nondetPercentage() { + int x = CProver.nondetInt(); + CProver.assume(x >= 0 && x <= 100); + return x; +} + +// Generate positive integer +public static int nondetPositive() { + int x = CProver.nondetInt(); + CProver.assume(x > 0); + return x; +} + +// Generate non-null array with size constraint +public static int[] nondetArray(int minSize, int maxSize) { + int[] arr = CProver.nondetWithoutNull(); + CProver.assume(arr.length >= minSize && arr.length <= maxSize); + return arr; +} +``` + +--- + +## Common Pitfalls + +### ❌ Don't: Use assertion to constrain input +```java +int x = CProver.nondetInt(); +assert x > 0; // WRONG! This will fail +``` + +### ✅ Do: Use assumption to constrain input +```java +int x = CProver.nondetInt(); +CProver.assume(x > 0); // CORRECT +assert x > 0; // Now this succeeds +``` + +--- + +### ❌ Don't: Assume after assert +```java +int x = CProver.nondetInt(); +assert x == 100; // WRONG! Too early +CProver.assume(x == 100); // Too late +``` + +### ✅ Do: Assume before assert +```java +int x = CProver.nondetInt(); +CProver.assume(x == 100); // Constrain first +assert x == 100; // Then verify +``` + +--- + +### ❌ Don't: Create unsatisfiable assumptions +```java +int x = CProver.nondetInt(); +CProver.assume(x > 100); +CProver.assume(x < 50); // WRONG! Contradictory +// All assertions will pass vacuously! +``` + +### ✅ Do: Ensure assumptions are satisfiable +```java +int x = CProver.nondetInt(); +CProver.assume(x > 50 && x < 100); // CORRECT - satisfiable +``` + +--- + +## Cheat Sheet + +```java +import org.cprover.CProver; + +// Non-determinism - create arbitrary values +int x = CProver.nondetInt(); +String s = CProver.nondetWithNull(); + +// Assumptions - constrain inputs +CProver.assume(x > 0 && x < 100); +CProver.assume(s != null); + +// Assertions - verify properties +assert x > 0 : "x is positive"; +assert s.length() >= 0 : "length is non-negative"; +``` + +--- + +## More Information + +- [Full Documentation](../java-modeling-constructs.md) +- [Examples Directory](.) +- [JBMC User Manual](../jbmc-user-manual.md) diff --git a/doc/cprover-manual/examples/README.md b/doc/cprover-manual/examples/README.md new file mode 100644 index 00000000000..027599bba92 --- /dev/null +++ b/doc/cprover-manual/examples/README.md @@ -0,0 +1,145 @@ +# Java Modeling Constructs Examples + +This directory contains example Java files demonstrating the use of fundamental +modeling constructs for JBMC verification. + +## Files + +- **`BankingExample.java`** - Complete example showing assertions, non-determinism, and assumptions +- **`AssertionExamples.java`** - Various assertion patterns and usage +- **`NondeterminismExamples.java`** - Examples of all non-deterministic value types +- **`AssumptionExamples.java`** - Comprehensive examples of using assumptions +- **`org/cprover/CProver.java`** - Stub implementation of the CProver class for compilation + +## Compiling the Examples + +To compile these examples for regular Java execution: + +```bash +javac *.java +``` + +Note: The examples will throw RuntimeException if executed normally. They are +designed to be analyzed with JBMC. + +## Running JBMC on the Examples + +To verify an example with JBMC, you need to specify the function to use as an +entry point: + +```bash +# Example 1: Verify the banking example +jbmc BankingExample --function BankingExample.verifyTransfer + +# Example 2: Verify mathematical properties +jbmc AssertionExamples --function AssertionExamples.mathematicalProperties + +# Example 3: Verify the absolute value function +jbmc NondeterminismExamples --function NondeterminismExamples.verifyAbsolute + +# Example 4: Test safe division +jbmc AssumptionExamples --function AssumptionExamples.testSafeDivide +``` + +## Common JBMC Options + +When running JBMC, you may want to use these options: + +- `--function ` - Specify the entry point function +- `--unwind ` - Set loop unwinding bound +- `--trace` - Show a counterexample trace if verification fails +- `--throw-runtime-exceptions` - Enable runtime exception checking + +Example with options: + +```bash +jbmc NondeterminismExamples \ + --function NondeterminismExamples.testPrimeCounter \ + --unwind 20 \ + --trace +``` + +## Understanding the Output + +JBMC will report: + +- **SUCCESS** - The property holds for all possible inputs +- **FAILURE** - Found a counterexample that violates the property +- With `--trace`, you'll see the specific input values that cause a failure + +## Key Concepts + +### Assertions +Use `assert` statements to specify properties you want to verify: +```java +assert x > 0 : "x must be positive"; +``` + +### Non-determinism +Use `CProver.nondetXXX()` methods to model arbitrary inputs: +```java +int x = CProver.nondetInt(); // x can be any integer +``` + +### Assumptions +Use `CProver.assume()` to constrain the search space: +```java +CProver.assume(x >= 0 && x <= 100); // only consider x in [0, 100] +``` + +## Tips for Writing Verification Harnesses + +1. **Start with small ranges** - Constrain inputs to reasonable ranges to avoid + state explosion: + ```java + int x = CProver.nondetInt(); + CProver.assume(x >= 0 && x <= 1000); + ``` + +2. **Use helper functions** - Create helper functions for common patterns: + ```java + public static int nondetPositive() { + int x = CProver.nondetInt(); + CProver.assume(x > 0); + return x; + } + ``` + +3. **Add descriptive messages** - Include clear messages with assertions: + ```java + assert result >= 0 : "result must be non-negative"; + ``` + +4. **Separate verification from production** - Keep verification harnesses + separate from production code + +5. **Check satisfiability** - Ensure your assumptions are satisfiable (not + contradictory) + +## Further Reading + +See the main documentation: +- [Java Modeling Constructs](../java-modeling-constructs.md) - Complete guide +- [JBMC User Manual](../jbmc-user-manual.md) - General JBMC usage +- [CBMC Tutorial](../cbmc-tutorial.md) - Basic tutorial + +## Troubleshooting + +### "Cannot execute CProver.XXX()" Runtime Error +This is expected! These examples are meant to be analyzed with JBMC, not +executed with regular Java. + +### Verification Takes Too Long +Try: +- Reducing input ranges with tighter assumptions +- Using smaller unwind bounds for loops +- Simplifying the property being checked + +### All Properties Pass Vacuously +Check that your assumptions are satisfiable. Contradictory assumptions will +cause all properties to pass vacuously. + +## Contributing + +If you have additional examples that would be helpful, please contribute them +following the existing style and structure. diff --git a/doc/cprover-manual/examples/org/cprover/CProver.java b/doc/cprover-manual/examples/org/cprover/CProver.java new file mode 100644 index 00000000000..d763cf81453 --- /dev/null +++ b/doc/cprover-manual/examples/org/cprover/CProver.java @@ -0,0 +1,204 @@ +package org.cprover; + +/** + * CProver class providing modeling constructs for JBMC verification. + * + * This class provides methods for: + * - Generating non-deterministic values (for modeling arbitrary inputs) + * - Making assumptions (for constraining the search space) + * - Additional JBMC-specific utilities + * + * Note: These methods have special meaning to JBMC and should not be + * executed in a regular Java runtime. They are for verification purposes only. + */ +public final class CProver { + + public static final boolean enableAssume = true; + + // ==== Non-deterministic Primitive Types ==== + + /** + * Returns an arbitrary boolean value. + * JBMC will explore both true and false. + */ + public static boolean nondetBoolean() { + throw new RuntimeException("Cannot execute CProver.nondetBoolean() - use JBMC for verification"); + } + + /** + * Returns an arbitrary byte value. + * JBMC will consider all possible byte values. + */ + public static byte nondetByte() { + throw new RuntimeException("Cannot execute CProver.nondetByte() - use JBMC for verification"); + } + + /** + * Returns an arbitrary char value. + * JBMC will consider all possible char values. + */ + public static char nondetChar() { + throw new RuntimeException("Cannot execute CProver.nondetChar() - use JBMC for verification"); + } + + /** + * Returns an arbitrary short value. + * JBMC will consider all possible short values. + */ + public static short nondetShort() { + throw new RuntimeException("Cannot execute CProver.nondetShort() - use JBMC for verification"); + } + + /** + * Returns an arbitrary int value. + * JBMC will consider all possible int values. + */ + public static int nondetInt() { + throw new RuntimeException("Cannot execute CProver.nondetInt() - use JBMC for verification"); + } + + /** + * Returns an arbitrary long value. + * JBMC will consider all possible long values. + */ + public static long nondetLong() { + throw new RuntimeException("Cannot execute CProver.nondetLong() - use JBMC for verification"); + } + + /** + * Returns an arbitrary float value. + * JBMC will consider all possible float values. + */ + public static float nondetFloat() { + throw new RuntimeException("Cannot execute CProver.nondetFloat() - use JBMC for verification"); + } + + /** + * Returns an arbitrary double value. + * JBMC will consider all possible double values. + */ + public static double nondetDouble() { + throw new RuntimeException("Cannot execute CProver.nondetDouble() - use JBMC for verification"); + } + + // ==== Non-deterministic Objects ==== + + /** + * Returns an arbitrary object of the inferred type. + * The returned object MAY be null. + * + * Example: + * String s = CProver.nondetWithNull(); + * // s might be null or a valid String + * + * @param the type of object to return + * @return an arbitrary object that may be null + */ + @SuppressWarnings("unchecked") + public static T nondetWithNull() { + throw new RuntimeException("Cannot execute CProver.nondetWithNull() - use JBMC for verification"); + } + + /** + * Returns an arbitrary object of the inferred type. + * The returned object is guaranteed to NOT be null. + * + * Example: + * String s = CProver.nondetWithoutNull(); + * // s is guaranteed to be a valid String (not null) + * + * @param the type of object to return + * @return an arbitrary non-null object + */ + @SuppressWarnings("unchecked") + public static T nondetWithoutNull() { + throw new RuntimeException("Cannot execute CProver.nondetWithoutNull() - use JBMC for verification"); + } + + // ==== Assumptions ==== + + /** + * Makes an assumption that restricts the search space. + * + * Only program executions where the condition evaluates to true + * will be considered by JBMC. + * + * Example: + * int x = CProver.nondetInt(); + * CProver.assume(x >= 0 && x <= 100); + * // Now JBMC only considers values where 0 <= x <= 100 + * + * Important: Assumptions are NOT checks! They constrain the input space. + * Use assertions (assert statement) to check properties. + * + * @param condition the condition to assume + */ + public static void assume(boolean condition) { + if (enableAssume) { + throw new RuntimeException("Cannot execute CProver.assume() - use JBMC for verification"); + } + } + + // ==== Concurrency Support ==== + + /** + * Returns the number of times the monitor (lock) is held on the given object. + * Used for verifying synchronization properties. + * + * @param obj the object to check + * @return the monitor count for the object + */ + public static int getMonitorCount(Object obj) { + throw new RuntimeException("Cannot execute CProver.getMonitorCount() - use JBMC for verification"); + } + + /** + * Marks the beginning of an atomic block. + * Used for concurrency verification. + */ + public static void atomicBegin() { + throw new RuntimeException("Cannot execute CProver.atomicBegin() - use JBMC for verification"); + } + + /** + * Marks the end of an atomic block. + * Used for concurrency verification. + */ + public static void atomicEnd() { + throw new RuntimeException("Cannot execute CProver.atomicEnd() - use JBMC for verification"); + } + + /** + * Marks the start of a new thread for verification purposes. + */ + public static void startThread() { + throw new RuntimeException("Cannot execute CProver.startThread() - use JBMC for verification"); + } + + /** + * Marks the end of a thread for verification purposes. + */ + public static void endThread() { + throw new RuntimeException("Cannot execute CProver.endThread() - use JBMC for verification"); + } + + /** + * Returns an arbitrary thread ID for the current thread. + * Used in concurrency verification. + * + * @return an arbitrary thread identifier + */ + public static int getCurrentThreadId() { + throw new RuntimeException("Cannot execute CProver.getCurrentThreadId() - use JBMC for verification"); + } + + // ==== Other Utilities ==== + + /** + * Indicates that a method is not modeled and its behavior is unknown. + * Used as a placeholder for unmodeled library methods. + */ + public static void notModelled() { + throw new RuntimeException("Cannot execute CProver.notModelled() - use JBMC for verification"); + } +} diff --git a/doc/cprover-manual/examples/test-compilation.sh b/doc/cprover-manual/examples/test-compilation.sh new file mode 100755 index 00000000000..48a97c2887c --- /dev/null +++ b/doc/cprover-manual/examples/test-compilation.sh @@ -0,0 +1,42 @@ +#!/bin/bash +# Test script to verify that all example files compile correctly + +set -e # Exit on first error + +echo "Testing Java Modeling Constructs Examples Compilation" +echo "=======================================================" +echo "" + +# Compile CProver class +echo "1. Compiling CProver class..." +javac org/cprover/CProver.java +echo " ✓ CProver.java compiled successfully" +echo "" + +# Compile example files +echo "2. Compiling example files..." + +echo " - BankingExample.java" +javac -cp . BankingExample.java + +echo " - AssertionExamples.java" +javac -cp . AssertionExamples.java + +echo " - NondeterminismExamples.java" +javac -cp . NondeterminismExamples.java + +echo " - AssumptionExamples.java" +javac -cp . AssumptionExamples.java + +echo " ✓ All examples compiled successfully" +echo "" + +echo "=======================================================" +echo "All compilation tests passed!" +echo "" +echo "Note: These examples are meant to be analyzed with JBMC," +echo "not executed with regular Java. Running them will throw" +echo "RuntimeException." +echo "" +echo "To verify with JBMC, use commands like:" +echo " jbmc BankingExample --function BankingExample.verifyTransfer" diff --git a/doc/cprover-manual/index.md b/doc/cprover-manual/index.md index 12e1a9c046b..48821e6d5e8 100644 --- a/doc/cprover-manual/index.md +++ b/doc/cprover-manual/index.md @@ -26,14 +26,19 @@ * [Memory-mapped I/O](modeling/mmio/) * [Shadow Memory](modeling/shadow-memory/) -8. Build Systems +8. JBMC – Java Bounded Model Checking + + * [JBMC User Manual](jbmc-user-manual/) + * [Java Modeling Constructs](java-modeling-constructs/) + +9. Build Systems * [Integration into Build Systems with goto-cc](goto-cc/) * [Integration with Visual Studio builds](visual-studio/) -9. [The CPROVER API Reference](api/) +10. [The CPROVER API Reference](api/) -10. Background Information on selected Command-line Options +11. Background Information on selected Command-line Options * [Incremental SMT solver](smt2-incr/) * [Unsound options](unsound_options/) diff --git a/doc/cprover-manual/java-modeling-constructs.md b/doc/cprover-manual/java-modeling-constructs.md new file mode 100644 index 00000000000..df51b77936d --- /dev/null +++ b/doc/cprover-manual/java-modeling-constructs.md @@ -0,0 +1,565 @@ +[CPROVER Manual TOC](../../) + +## Fundamental Modeling Constructs for Java + +This document explains how to use fundamental modeling constructs in Java when +working with JBMC (Java Bounded Model Checker). These constructs allow you to +write verification harnesses and specify properties that JBMC will check +exhaustively. + +### Table of Contents + +1. [Assertions](#assertions) +2. [Non-determinism](#non-determinism) +3. [Assumptions](#assumptions) +4. [Complete Example](#complete-example) + +--- + +## Assertions + +Assertions are used to specify properties that should hold in your program. +JBMC will verify that these properties are true for all possible program +executions. + +### Using Java's Standard `assert` Keyword + +The simplest way to specify properties is using Java's built-in `assert` +statement: + +```java +public class AssertExample { + public static void checkPositive(int x) { + assert x > 0 : "x must be positive"; + } +} +``` + +When JBMC analyzes this code, it will verify that the assertion holds for all +possible values of `x`. If the assertion can be violated, JBMC will report a +failure and provide a counterexample. + +**Key Points:** +- The assertion message (after the colon) is optional but recommended for + clarity +- JBMC checks assertions statically for **all** possible inputs +- Unlike runtime assertion checking, JBMC does not require the `-ea` flag + +### Example: Array Bounds Safety + +```java +public class ArrayExample { + public static void accessArray(int[] arr, int index) { + // JBMC automatically checks array bounds, but you can add explicit + // assertions for clarity + assert index >= 0 && index < arr.length : "index is within bounds"; + int value = arr[index]; + assert value >= 0 : "array contains non-negative values"; + } +} +``` + +--- + +## Non-determinism + +Non-determinism allows you to model arbitrary or unknown input values. This is +essential for verification because it enables JBMC to check your code against +**all possible inputs**, not just specific test cases. + +### The `org.cprover.CProver` Class + +JBMC provides the `org.cprover.CProver` class with methods for generating +non-deterministic values. These methods return arbitrary values of their +respective types. + +### Primitive Type Non-determinism + +The following methods are available for primitive types: + +```java +import org.cprover.CProver; + +public class NondetExample { + public static void demonstrateNondet() { + // Generate non-deterministic primitive values + boolean b = CProver.nondetBoolean(); // arbitrary boolean + byte by = CProver.nondetByte(); // arbitrary byte + char c = CProver.nondetChar(); // arbitrary char + short s = CProver.nondetShort(); // arbitrary short + int i = CProver.nondetInt(); // arbitrary int + long l = CProver.nondetLong(); // arbitrary long + float f = CProver.nondetFloat(); // arbitrary float + double d = CProver.nondetDouble(); // arbitrary double + } +} +``` + +**Important Notes:** +- These methods have no implementation body - they are recognized and handled + specially by JBMC +- Non-deterministic values represent **all possible** values of that type +- Non-determinism is **not** the same as randomness; it's universal + quantification over all possible values + +### Object Non-determinism + +For reference types (objects), JBMC provides two methods: + +```java +import org.cprover.CProver; + +public class ObjectNondetExample { + public static void demonstrateObjectNondet() { + // Non-deterministic object that CAN be null + String s1 = CProver.nondetWithNull(); + // s1 might be null or might be a valid String object + + // Non-deterministic object that CANNOT be null + String s2 = CProver.nondetWithoutNull(); + // s2 is guaranteed to be a valid String object (not null) + } +} +``` + +**Key Differences:** +- `nondetWithNull()` - returns an arbitrary object that may or may not be null +- `nondetWithoutNull()` - returns an arbitrary object that is guaranteed to be + non-null + +### Practical Example: Verifying a Division Function + +```java +import org.cprover.CProver; + +public class DivisionExample { + public static int safeDivide(int numerator, int denominator) { + if (denominator == 0) { + return 0; // or throw an exception + } + return numerator / denominator; + } + + public static void verifyDivision() { + // Generate arbitrary inputs + int a = CProver.nondetInt(); + int b = CProver.nondetInt(); + + // Call the function + int result = safeDivide(a, b); + + // Verify properties + if (b != 0) { + assert result == a / b : "division is correct"; + } else { + assert result == 0 : "division by zero returns 0"; + } + } +} +``` + +--- + +## Assumptions + +Assumptions are used to restrict the search space by constraining non-deterministic +inputs. They tell JBMC: "only consider program executions where this condition +holds." + +### The `CProver.assume()` Method + +```java +import org.cprover.CProver; + +public class AssumeExample { + public static void demonstrateAssume() { + int x = CProver.nondetInt(); + + // Restrict x to be in the range [1, 100] + CProver.assume(x >= 1 && x <= 100); + + // Now JBMC will only consider values where 1 <= x <= 100 + assert x > 0 : "x is positive"; // This will succeed + assert x <= 100 : "x is at most 100"; // This will succeed + } +} +``` + +### Assumptions vs. Assertions + +It's crucial to understand the difference: + +- **Assertion**: "I claim this property MUST hold" + - If violated, JBMC reports a verification failure + - Used to specify **what you want to prove** + +- **Assumption**: "Only consider cases where this holds" + - Cannot be violated - constrains the search space + - Used to specify **preconditions** or **input constraints** + +### Example: Comparing Assumptions and Assertions + +```java +import org.cprover.CProver; + +public class AssumeVsAssert { + // INCORRECT: This will fail + public static void incorrectUse() { + int x = CProver.nondetInt(); + assert x > 0; // FAILS: x can be negative or zero + } + + // CORRECT: Use assume to constrain the input + public static void correctUse() { + int x = CProver.nondetInt(); + CProver.assume(x > 0); // Only consider positive x + assert x > 0; // SUCCEEDS: x is constrained to be positive + } +} +``` + +### Warning: Ensure Assumptions are Satisfiable + +Always ensure your assumptions can be satisfied. Unsatisfiable assumptions lead +to vacuous verification: + +```java +import org.cprover.CProver; + +public class UnsatisfiableExample { + public static void vacuousVerification() { + int x = CProver.nondetInt(); + + // These assumptions are contradictory! + CProver.assume(x > 100); + CProver.assume(x < 50); + + // This will "succeed" but vacuously - there are no valid inputs + assert false; // Incorrectly passes! + } +} +``` + +### Assumptions are Non-Retroactive + +Assumptions only affect assertions that follow them in program order: + +```java +import org.cprover.CProver; + +public class AssumptionOrderExample { + // INCORRECT: Assumption comes after assertion + public static void wrongOrder() { + int x = CProver.nondetInt(); + assert x == 100; // FAILS: x is not constrained yet + CProver.assume(x == 100); // Too late! + } + + // CORRECT: Assumption comes before assertion + public static void correctOrder() { + int x = CProver.nondetInt(); + CProver.assume(x == 100); // Constrain first + assert x == 100; // SUCCEEDS: x is now constrained + } +} +``` + +### Practical Example: Constrained Array Access + +```java +import org.cprover.CProver; + +public class ArrayAccessExample { + public static void safeArrayAccess(int[] arr) { + // Assume arr is non-null and has at least one element + CProver.assume(arr != null); + CProver.assume(arr.length > 0); + + int index = CProver.nondetInt(); + // Constrain index to valid range + CProver.assume(index >= 0 && index < arr.length); + + // This access is now guaranteed to be safe + int value = arr[index]; + assert value == arr[index]; // Trivially true, but demonstrates safety + } +} +``` + +### Common Pattern: Modeling Bounded Inputs + +A common use case is to model inputs within specific ranges: + +```java +import org.cprover.CProver; + +public class BoundedInputExample { + // Model a percentage (0-100) + public static int nondetPercentage() { + int percentage = CProver.nondetInt(); + CProver.assume(percentage >= 0 && percentage <= 100); + return percentage; + } + + // Model a positive integer + public static int nondetPositive() { + int value = CProver.nondetInt(); + CProver.assume(value > 0); + return value; + } + + public static void useConstrainedInputs() { + int pct = nondetPercentage(); + assert pct >= 0 && pct <= 100; // Always succeeds + + int pos = nondetPositive(); + assert pos > 0; // Always succeeds + } +} +``` + +--- + +## Complete Example + +Here's a complete example that demonstrates all three concepts together: + +```java +import org.cprover.CProver; + +/** + * Example: Verifying a simple banking operation + */ +public class BankingExample { + + /** + * Transfer money from one account to another + * @param fromBalance - source account balance + * @param toBalance - destination account balance + * @param amount - amount to transfer + * @return true if transfer succeeded, false otherwise + */ + public static boolean transfer(int fromBalance, int toBalance, int amount) { + if (amount <= 0) { + return false; // Invalid amount + } + if (fromBalance < amount) { + return false; // Insufficient funds + } + // Transfer successful + return true; + } + + /** + * Verification harness for the transfer function + */ + public static void verifyTransfer() { + // 1. NON-DETERMINISM: Create arbitrary inputs + int fromBalance = CProver.nondetInt(); + int toBalance = CProver.nondetInt(); + int amount = CProver.nondetInt(); + + // 2. ASSUMPTIONS: Constrain inputs to valid ranges + // Balances must be non-negative + CProver.assume(fromBalance >= 0); + CProver.assume(toBalance >= 0); + // Amount must be reasonable (prevent overflow) + CProver.assume(amount >= 0 && amount <= 1000000); + + // Call the function under test + boolean result = transfer(fromBalance, toBalance, amount); + + // 3. ASSERTIONS: Verify expected properties + + // Property 1: Transfer fails for non-positive amounts + if (amount <= 0) { + assert !result : "transfer should fail for non-positive amount"; + } + + // Property 2: Transfer fails for insufficient funds + if (amount > 0 && fromBalance < amount) { + assert !result : "transfer should fail for insufficient funds"; + } + + // Property 3: Transfer succeeds when conditions are met + if (amount > 0 && fromBalance >= amount) { + assert result : "transfer should succeed when funds are sufficient"; + } + } + + /** + * Example with object non-determinism + */ + public static void verifyWithObjects() { + // Create non-deterministic String that might be null + String message = CProver.nondetWithNull(); + + // Assume it's non-null for this test + CProver.assume(message != null); + + // Now we can safely use the string + int length = message.length(); + assert length >= 0 : "string length is non-negative"; + } + + public static void main(String[] args) { + // Run verification harnesses + verifyTransfer(); + verifyWithObjects(); + } +} +``` + +### Running JBMC on This Example + +To verify this example with JBMC: + +1. Compile the Java file: + ```bash + javac BankingExample.java + ``` + +2. Run JBMC: + ```bash + jbmc BankingExample + ``` + +3. JBMC will exhaustively check all assertions for all possible input + combinations (subject to the assumptions). + +--- + +## Best Practices + +### 1. Use Descriptive Assertion Messages + +```java +// Good +assert balance >= 0 : "account balance must be non-negative"; + +// Less helpful +assert balance >= 0; +``` + +### 2. Constrain Non-deterministic Inputs Appropriately + +```java +// Too loose - may cause state explosion +int x = CProver.nondetInt(); + +// Better - constrain to relevant range +int x = CProver.nondetInt(); +CProver.assume(x >= 0 && x <= 100); +``` + +### 3. Separate Test Logic from Production Code + +Keep your verification harnesses separate from production code: + +```java +// Production code +public class Calculator { + public static int add(int a, int b) { + return a + b; + } +} + +// Verification harness (separate file or test method) +public class CalculatorVerification { + public static void verifyAdd() { + int a = CProver.nondetInt(); + int b = CProver.nondetInt(); + // Add reasonable bounds + CProver.assume(a >= -1000 && a <= 1000); + CProver.assume(b >= -1000 && b <= 1000); + + int result = Calculator.add(a, b); + assert result == a + b; + } +} +``` + +### 4. Be Aware of State Space Explosion + +The number of states JBMC explores grows with: +- Number of non-deterministic choices +- Loop iterations +- Recursion depth +- Object complexity + +Use assumptions to keep the state space manageable. + +--- + +## Common Pitfalls + +### 1. Forgetting to Import CProver + +```java +// ERROR: CProver not imported +public class Example { + public static void test() { + int x = CProver.nondetInt(); // Compilation error! + } +} + +// CORRECT: Import the class +import org.cprover.CProver; + +public class Example { + public static void test() { + int x = CProver.nondetInt(); // OK + } +} +``` + +### 2. Using Assumptions Instead of Assertions + +```java +// WRONG: Using assume to check a property +public static void incorrectCheck(int x) { + CProver.assume(x > 0); // This doesn't check anything! +} + +// CORRECT: Use assert to check properties +public static void correctCheck(int x) { + assert x > 0 : "x must be positive"; // This checks the property +} +``` + +### 3. Creating Unsatisfiable Assumptions + +```java +// WRONG: Contradictory assumptions +int x = CProver.nondetInt(); +CProver.assume(x > 100); +CProver.assume(x < 0); +// No value of x can satisfy both constraints! +``` + +--- + +## Further Reading + +- [JBMC User Manual](jbmc-user-manual.md) - General JBMC usage +- [Modeling with Assumptions (C)](modeling-assumptions.md) - C language assumptions +- [Nondeterminism (C)](modeling-nondeterminism.md) - C language nondeterminism +- [CBMC Tutorial](cbmc-tutorial.md) - Basic CBMC/JBMC tutorial + +--- + +## Summary + +| Construct | Purpose | Example | +|-----------|---------|---------| +| **Assertion** | Specify properties to verify | `assert x > 0 : "x is positive";` | +| **Non-determinism** | Model arbitrary inputs | `int x = CProver.nondetInt();` | +| **Assumption** | Constrain input space | `CProver.assume(x > 0 && x < 100);` | + +Remember: +- **Assert** what you want to **prove** +- **Assume** what you want to **constrain** +- Use **non-determinism** to represent **arbitrary inputs** + +These three constructs form the foundation of writing effective verification +harnesses for JBMC. diff --git a/doc/cprover-manual/jbmc-user-manual.md b/doc/cprover-manual/jbmc-user-manual.md index e56c04036d9..2567418d1dd 100644 --- a/doc/cprover-manual/jbmc-user-manual.md +++ b/doc/cprover-manual/jbmc-user-manual.md @@ -157,6 +157,10 @@ INPUT inputVal: 15 The value chosen by JBMC is arbitrary, and could as well be 9 or 2084569161. +For a comprehensive guide on using assertions, non-determinism, and assumptions +in Java for JBMC, see the [Java Modeling Constructs](java-modeling-constructs.md) +documentation. + ## Java Library support The examples above only involve primitive types. In order to analyse code @@ -261,6 +265,10 @@ then be reported like any other uncaught exception. ## Further documentation +For more detailed information on fundamental modeling constructs in Java for +JBMC (assertions, non-determinism, and assumptions), see: +- [Java Modeling Constructs](java-modeling-constructs.md) - Comprehensive guide with examples + JBMC has a wealth of other options that can either constrain the model (to cope with complexity issues), or output more relevant information. The list of all available options is printed by running: