static-reasoning-verifier

Static Reasoning Verifier

Verify code correctness statically against specifications through type checking, contract verification, and formal reasoning.

Quick Start

Verify Python Code

# Type checking and contract verification
python scripts/verify_python.py src/app.py

# Strict mode (enforce all type annotations)
python scripts/verify_python.py src/ --strict

Verify Java Code

# Type checking, null safety, and JML contracts
python scripts/verify_java.py src/Main.java

# Strict mode (enforce JML contracts)
python scripts/verify_java.py src/ --strict

Verification Types

1. Type Checking

Verify type correctness using static type checkers:

Python (mypy):

def add(a: int, b: int) -> int:
    return a + b

result: int = add(5, 10)  # ✅ Type safe
result: str = add(5, 10)  # ❌ Type error

Java:

public int add(int a, int b) {
    return a + b;
}

int result = add(5, 10);    // ✅ Type safe
String result = add(5, 10); // ❌ Compile error

2. Contract Verification

Verify preconditions, postconditions, and invariants:

Python:

def sqrt(x: float) -> float:
    """
    Calculate square root.

    Requires:
        - x >= 0

    Ensures:
        - result * result ≈ x
    """
    assert x >= 0, "Input must be non-negative"
    result = x ** 0.5
    assert abs(result * result - x) < 1e-10
    return result

Java (JML):

/*@ requires x >= 0;
  @ ensures \result >= 0;
  @ ensures \result * \result <= x;
  @*/
public static int sqrt(int x) {
    // Implementation
}

3. Null Safety

Verify null pointer safety:

Java:

public @NonNull String getName(@NonNull User user) {
    return user.getName();  // Safe - user cannot be null
}

Python:

from typing import Optional

def find_user(user_id: int) -> Optional[User]:
    """May return None if user not found."""
    return database.get_user(user_id)

Verification Workflow

1. Write Specifications

Define contracts for functions/methods:

def divide(a: float, b: float) -> float:
    """
    Divide two numbers.

    Precondition:
        - b != 0

    Postcondition:
        - result * b ≈ a

    Raises:
        ValueError: If b is zero
    """
    if b == 0:
        raise ValueError("Division by zero")
    return a / b

2. Add Type Annotations

from typing import List, Optional

def process_items(items: List[int], threshold: int = 0) -> List[int]:
    """Filter items above threshold."""
    return [item for item in items if item > threshold]

3. Run Verification

# Verify implementation matches specifications
python scripts/verify_python.py src/

4. Review Issues

Found 3 issue(s): 1 error(s), 2 warning(s)

ERRORS:
  ❌ src/utils.py:15 [type]
     Argument 1 to "divide" has incompatible type "str"; expected "float"
     💡 Check argument type matches function signature

WARNINGS:
  ⚠️  src/math.py:42 [contract]
     Function 'sqrt' has parameters but no preconditions specified
     💡 Add 'Requires:' section in docstring or @requires decorator

5. Fix Issues

Update code to satisfy specifications:

# Before (type error)
result = divide("10", 5)

# After (type safe)
result = divide(10.0, 5.0)

Python Verification

Type Checking with mypy

The verification script uses mypy for static type checking:

python scripts/verify_python.py src/ --strict

Checks:

• Type compatibility
• Function signatures
• Return types
• Optional/None handling

Example:

def greet(name: str) -> str:
    return f"Hello, {name}"

greet("Alice")  # ✅ Valid
greet(123)      # ❌ Type error: expected str, got int

Contract Verification

Checks design-by-contract specifications:

Decorator-based:

from contracts import requires, ensures

@requires(lambda x: x >= 0)
@ensures(lambda result: result >= 0)
def sqrt(x: float) -> float:
    return x ** 0.5

Docstring-based:

def withdraw(account: Account, amount: float) -> None:
    """
    Withdraw money from account.

    Requires:
        - amount > 0
        - amount <= account.balance

    Ensures:
        - account.balance == old(account.balance) - amount
    """
    assert amount > 0
    assert amount <= account.balance
    account.balance -= amount

See [python_contracts.md](references/python_contracts.md) for complete guide on Python design-by-contract patterns.

Java Verification

Type and Null Safety

The verification script uses javac for compilation and type checking:

python scripts/verify_java.py src/ --strict

Checks:

• Type compatibility
• Null safety annotations (@NonNull, @Nullable)
• Method signatures
• Generic type parameters

Example:

public @NonNull String formatUser(@NonNull User user) {
    // user cannot be null
    return user.getName() + " (" + user.getEmail() + ")";
}

public @Nullable User findUser(int userId) {
    // May return null
    return database.getUser(userId);
}

JML Contract Verification

Checks Java Modeling Language specifications:

public class BankAccount {
    private double balance;

    /*@ invariant balance >= 0;
      @*/

    /*@ requires amount > 0;
      @ requires amount <= balance;
      @ ensures balance == \old(balance) - amount;
      @ assignable balance;
      @*/
    public void withdraw(double amount) {
        balance -= amount;
    }

    /*@ requires amount > 0;
      @ ensures balance == \old(balance) + amount;
      @ assignable balance;
      @*/
    public void deposit(double amount) {
        balance += amount;
    }
}

See [java_jml.md](references/java_jml.md) for complete JML specification guide.

Common Verification Patterns

Range Validation

def set_age(person: Person, age: int) -> None:
    """
    Requires: 0 <= age <= 150
    Ensures: person.age == age
    """
    assert 0 <= age <= 150, "Age must be between 0 and 150"
    person.age = age

Collection Constraints

def process_batch(items: List[Item]) -> None:
    """
    Requires:
        - len(items) > 0
        - len(items) <= 1000
    """
    assert len(items) > 0, "Batch cannot be empty"
    assert len(items) <= 1000, "Batch too large"
    # Process items

State Invariants

class Stack:
    """
    Invariant:
        - 0 <= self.size <= self.capacity
        - All elements before size are not None
    """

    def push(self, item):
        """
        Requires: not self.is_full() and item is not None
        Ensures: self.size == old(self.size) + 1
        """
        assert not self.is_full()
        assert item is not None
        self.items[self.size] = item
        self.size += 1
        self._check_invariant()

Best Practices

1. Write Contracts First

Define specifications before implementation:

def sort_list(items: List[int]) -> List[int]:
    """
    Sort list in ascending order.

    Requires:
        - items is a list

    Ensures:
        - len(result) == len(items)
        - result is sorted ascending
        - result contains same elements as items
    """
    # Implementation here

2. Keep Contracts Simple

# ✅ Good - Simple, clear
def withdraw(amount: float):
    """Requires: amount > 0 and amount <= balance"""
    assert amount > 0 and amount <= self.balance

# ❌ Bad - Too complex
def withdraw(amount: float):
    """Requires: (amount > 0 and amount <= balance) or (overdraft_allowed and amount <= balance + overdraft_limit)"""

3. Use Type Annotations Consistently

# ✅ Good - All parameters and return types annotated
def calculate_total(items: List[Item], tax_rate: float) -> float:
    return sum(item.price for item in items) * (1 + tax_rate)

# ❌ Bad - Missing annotations
def calculate_total(items, tax_rate):
    return sum(item.price for item in items) * (1 + tax_rate)

4. Verify E