static-reasoning-verifier

name

static-reasoning-verifier

description

Verify code correctness statically against specifications using type checking, contract verification, and formal methods. Use when: (1) Verifying type safety and null safety in Python, Java, or C/C++ code, (2) Checking design-by-contract specifications (preconditions, postconditions, invariants), (3) Validating code against formal specifications, (4) Ensuring code quality and correctness before runtime, (5) Finding potential bugs through static analysis. Supports Python (mypy, contracts), Java (javac, JML), and provides verification scripts and contract specification guidelines.

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 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 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 Early and Often

# Verify after every significant change
python scripts/verify_python.py src/

# Integrate into CI/CD
make verify  # Run verification in build pipeline

5. Document Side Effects

def update_database(user: User) -> None:
    """
    Update user in database.

    Requires:
        - user.id is set

    Ensures:
        - Database contains updated user

    Side effects:
        - Modifies database
        - May raise DatabaseError
    """

Troubleshooting

Type Errors

Problem: Incompatible type error

Solution:

# Add explicit type annotation or cast
result: int = int(value)  # Cast to int
result = cast(int, value)  # Type cast

Problem: Optional type handling

Solution:

def get_name(user: Optional[User]) -> str:
    if user is None:
        return "Unknown"
    return user.name  # Safe - checked for None

Contract Violations

Problem: Precondition failure

Solution:

# Add validation before calling
if amount > 0 and amount <= account.balance:
    account.withdraw(amount)
else:
    raise ValueError("Invalid withdrawal amount")

Problem: Postcondition failure

Solution:

# Verify implementation satisfies postcondition
def sqrt(x: float) -> float:
    result = x ** 0.5
    # Check postcondition
    assert abs(result * result - x) < 1e-10
    return result

Reference Documentation

Python Contracts

See python_contracts.md for:

• Design by contract patterns
• Preconditions, postconditions, invariants
• Decorator-based contracts (icontract, deal)
• Docstring specifications
• Type annotations as contracts
• Common contract patterns
• Verification checklist

Java JML

See java_jml.md for:

• JML syntax and semantics
• Preconditions (@requires)
• Postconditions (@ensures)
• Class invariants
• Quantifiers and pure methods
• Assignable clauses
• Null safety with JML
• OpenJML verification tools
• Loop invariants
• Contract inheritance

Integration with Development Workflow

Pre-commit Hook

#!/bin/bash
# .git/hooks/pre-commit

echo "Running static verification..."
python scripts/verify_python.py src/

if [ $? -ne 0 ]; then
    echo "Verification failed. Commit aborted."
    exit 1
fi

CI/CD Pipeline

# .github/workflows/verify.yml
name: Static Verification

on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3

      - name: Set up Python
        uses: actions/setup-python@v4
        with:
          python-version: '3.11'

      - name: Install dependencies
        run: pip install mypy

      - name: Run verification
        run: python scripts/verify_python.py src/ --strict

IDE Integration

Most IDEs support type checking and linting:

• VS Code: Python extension with mypy integration
• PyCharm: Built-in type checker
• IntelliJ IDEA: Java type checking and JML plugins