Specification Generator

def withdraw(account, amount):
    if account.balance < amount:
        raise InsufficientFundsError()
    account.balance -= amount
    return account.balance

# withdraw function
Preconditions:
- account is not None
- amount > 0
- account.balance >= amount (to succeed without exception)

Postconditions:
- If successful: account.balance == old(account.balance) - amount
- If successful: return value == new balance
- If insufficient: raises InsufficientFundsError
- account object still valid

Invariants (Account class):
- balance >= 0 (always)
- account_number is immutable

/*@ requires amount > 0;
  @ requires account != null;
  @ requires account.balance >= amount;
  @ ensures account.balance == \old(account.balance) - amount;
  @ ensures \result == account.balance;
  @ signals (InsufficientFundsError e) account.balance < amount;
  @*/
public int withdraw(Account account, int amount) {
    // implementation
}

/*@ requires amount > 0;
  @ requires \valid(account);
  @ requires account->balance >= amount;
  @ ensures account->balance == \old(account->balance) - amount;
  @ ensures \result == account->balance;
  @*/
int withdraw(Account *account, int amount) {
    // implementation
}

method Withdraw(account: Account, amount: int) returns (newBalance: int)
    requires amount > 0
    requires account.balance >= amount
    ensures account.balance == old(account.balance) - amount
    ensures newBalance == account.balance
    modifies account
{
    // implementation
}

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

    :param account: The account to withdraw from
    :param amount: The amount to withdraw (must be positive)
    :raises InsufficientFundsError: If balance < amount
    :raises ValueError: If amount <= 0
    :returns: The new account balance

    Preconditions:
        - account is not None
        - amount > 0
        - account.balance >= amount (for successful withdrawal)

    Postconditions:
        - account.balance == old_balance - amount
        - return value == account.balance
        - If insufficient funds: InsufficientFundsError raised
        - account.balance >= 0 (invariant preserved)
    """
    # implementation

# Test preconditions
assert amount > 0  # Valid
assert account is not None  # Valid
assert account.balance >= amount  # Valid for success case

# Test postconditions
old_balance = account.balance
result = withdraw(account, 100)
assert account.balance == old_balance - 100  # Check
assert result == account.balance  # Check

# Test invariants
assert account.balance >= 0  # Should always hold

def sqrt(x):
    """Compute square root."""
    return x ** 0.5

def sqrt(x: float) -> float:
    """
    Compute the square root of x.

    :param x: The number to compute square root of
    :returns: The square root of x
    :raises ValueError: If x < 0

    Preconditions:
        - x >= 0

    Postconditions:
        - result >= 0
        - abs(result * result - x) < 1e-10  # Precision tolerance
        - If x == 0, then result == 0
        - If x == 1, then result == 1
    """
    if x < 0:
        raise ValueError("Cannot compute square root of negative number")
    return x ** 0.5

/*@ requires x >= 0;
  @ ensures \result >= 0;
  @ ensures Math.abs(\result * \result - x) < 1e-10;
  @ ensures x == 0 ==> \result == 0;
  @ ensures x == 1 ==> \result == 1;
  @ signals (IllegalArgumentException e) x < 0;
  @*/
public double sqrt(double x) {
    if (x < 0) throw new IllegalArgumentException();
    return Math.sqrt(x);
}

def sort_list(items):
    """Sort list in-place."""
    items.sort()

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

    :param items: List to sort (modified in-place)

    Preconditions:
        - items is not None
        - All elements in items are comparable

    Postconditions:
        - len(items) == len(old(items))  # Same length
        - set(items) == set(old(items))  # Same elements
        - For all i, j: i < j implies items[i] <= items[j]  # Sorted
        - items is sorted in ascending order

    Frame conditions:
        - Only items is modified
        - No other data structures affected
    """
    if items is None:
        raise ValueError("items cannot be None")
    items.sort()

/*@ requires \valid(arr + (0..len-1));
  @ ensures \forall integer i, j;
  @     0 <= i < j < len ==> arr[i] <= arr[j];
  @ ensures Permutation{Pre,Post}(arr, 0, len-1);
  @ assigns arr[0..len-1];
  @*/
void sort_array(int *arr, int len) {
    // implementation
}

class BankAccount:
    def __init__(self, account_number, initial_balance):
        self.account_number = account_number
        self.balance = initial_balance

    def deposit(self, amount):
        self.balance += amount

    def withdraw(self, amount):
        if self.balance < amount:
            raise InsufficientFundsError()
        self.balance -= amount

class BankAccount:
    """
    Bank account with balance and account number.

    Class Invariants:
        - balance >= 0 (balance never negative)
        - account_number is immutable (never changes after init)
        - account_number is unique (within system)
    """

    def __init__(self, account_number: str, initial_balance: float) -> None:
        """
        Create new bank account.

        Preconditions:
            - account_number is not None and not empty
            - initial_balance >= 0
            - account_number not already in use

        Postconditions:
            - self.account_number == account_number
            - self.balance == initial_balance
            - Invariants established
        """
        if not account_number:
            raise ValueError("Account number required")
        if initial_balance < 0:
            raise ValueError("Initial balance cannot be negative")

        self.account_number = account_number
        self.balance = initial_balance

    def deposit(self, amount: float) -> None:
        """
        Deposit amount into account.

        Preconditions:
            - amount > 0
            - Invariants hold

        Postconditions:
            - self.balance == old(self.balance) + amount
            - Invariants still hold

        Frame conditions:
            - Only self.balance modified
            - account_number unchanged
        """
        if amount <= 0:
            raise ValueError("Deposit amount must be positive")
        self.balance += amount
        assert self.balance >= 0  # Invariant check

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

        Preconditions:
            - amount > 0
            - self.balance >= amount
            - Invariants hold

        Postconditions:
            - self.balance == old(self.balance) - amount
            - Invariants still hold

        Exceptional postconditions:
            - If balance < amount: InsufficientFundsError raised
            - If balance < amount: balance unchanged
        """
        if amount <= 0:
            raise ValueError("Withdrawal amount must be positive")
        if self.balance < amount:
            raise InsufficientFundsError()
        self.balance -= amount
        assert self.balance >= 0  # Invariant check

public class BankAccount {
    /*@ invariant balance >= 0;
      @ invariant account_number != null;
      @*/
    private /*@ spec_public @*/ double balance;
    private /*@ spec_public @*/ final String account_number;

    /*@ requires account_number != null;
      @ requires initial_balance >= 0;
      @ ensures this.account_number == account_number;
      @ ensures this.balance == initial_balance;
      @*/
    public BankAccount(String account_number, double initial_balance) {
        // implementation
    }

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

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

def sum_array(arr):
    total = 0
    for i in range(len(arr)):
        total += arr[i]
    return total

def sum_array(arr: List[int]) -> int:
    """
    Compute sum of all elements in array.

    Preconditions:
        - arr is not None

    Postconditions:
        - result == sum of all elements in arr
    """
    total = 0

    # Loop invariant:
    # - 0 <= i <= len(arr)
    # - total == sum(arr[0:i])
    # - total is sum of elements seen so far

    for i in range(len(arr)):
        # At this point:
        # - Invariant holds at loop entry
        # - i < len(arr)

        total += arr[i]

        # At this point:
        # - total == sum(arr[0:i+1])
        # - Invariant holds for next iteration

    # At loop exit:
    # - i == len(arr)
    # - total == sum(arr[0:len(arr)]) == sum(arr)

    return total

method SumArray(arr: array<int>) returns (total: int)
    requires arr != null
    ensures total == sum(arr[..])
{
    total := 0;
    var i := 0;

    while i < arr.Length
        invariant 0 <= i <= arr.Length
        invariant total == sum(arr[..i])
    {
        total := total + arr[i];
        i := i + 1;
    }
}

def binary_search(arr, target):
    left, right = 0, len(arr) - 1
    while left <= right:
        mid = (left + right) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            left = mid + 1
        else:
            right = mid - 1
    return -1

def binary_search(arr: List[int], target: int) -> int:
    """
    Search for target in sorted array using binary search.

    Preconditions:
        - arr is not None
        - arr is sorted in ascending order:
          For all i, j: 0 <= i < j < len(arr) implies arr[i] <= arr[j]

    Postconditions:
        - If result >= 0: arr[result] == target
        - If result >= 0: 0 <= result < len(arr)
        - If result == -1: target not in arr
        - If multiple occurrences: returns any valid index
    """
    if arr is None:
        raise ValueError("Array cannot be None")

    left, right = 0, len(arr) - 1

    # Loop invariant:
    # - 0 <= left <= right + 1 <= len(arr)
    # - If target in arr, then target in arr[left:right+1]
    # - All elements in arr[0:left] < target
    # - All elements in arr[right+1:] > target

    while left <= right:
        mid = (left + right) // 2

        if arr[mid] == target:
            # Postcondition: arr[mid] == target
            return mid
        elif arr[mid] < target:
            left = mid + 1
            # Invariant maintained: arr[0:left] < target
        else:
            right = mid - 1
            # Invariant maintained: arr[right+1:] > target

    # Loop exit: left > right
    # Invariant implies target not in arr
    return -1

/*@ requires \valid_read(arr + (0..len-1));
  @ requires Sorted(arr, 0, len-1);
  @
  @ behavior found:
  @   ensures 0 <= \result < len;
  @   ensures arr[\result] == target;
  @
  @ behavior not_found:
  @   ensures \result == -1;
  @   ensures \forall integer i; 0 <= i < len ==> arr[i] != target;
  @
  @ complete behaviors;
  @ disjoint behaviors;
  @*/
int binary_search(int *arr, int len, int target) {
    int left = 0, right = len - 1;

    /*@ loop invariant 0 <= left <= right + 1 <= len;
      @ loop invariant \forall integer i; 0 <= i < left ==> arr[i] < target;
      @ loop invariant \forall integer i; right < i < len ==> arr[i] > target;
      @ loop variant right - left;
      @*/
    while (left <= right) {
        int mid = left + (right - left) / 2;
        if (arr[mid] == target) return mid;
        else if (arr[mid] < target) left = mid + 1;
        else right = mid - 1;
    }
    return -1;
}

class Node:
    def __init__(self, data):
        self.data = data
        self.next = None

def reverse_list(head):
    prev = None
    current = head
    while current:
        next_node = current.next
        current.next = prev
        prev = current
        current = next_node
    return prev

class Node:
    """
    Linked list node.

    Invariants:
        - data can be any value
        - next is either None or a Node
    """
    def __init__(self, data: Any) -> None:
        """
        Create new node.

        Postconditions:
            - self.data == data
            - self.next == None
        """
        self.data = data
        self.next = None

def reverse_list(head: Optional[Node]) -> Optional[Node]:
    """
    Reverse a singly linked list in-place.

    Preconditions:
        - head is None or points to valid linked list
        - List is acyclic (no cycles)

    Postconditions:
        - Returns new head of reversed list
        - If head is None, returns None
        - Number of nodes unchanged
        - All data values preserved
        - Order of data values is reversed
        - Original list structure modified
        - If original: A -> B -> C -> None
          Then result: C -> B -> A -> None

    Frame conditions:
        - Only next pointers modified
        - data values unchanged
        - No new nodes created
        - No nodes deleted
    """
    prev = None
    current = head

    # Loop invariant:
    # - prev points to reversed portion
    # - current points to unreversed portion
    # - prev is reverse of head[0:processed]
    # - current is head[processed:]

    while current is not None:
        next_node = current.next
        current.next = prev
        prev = current
        current = next_node

        # Invariant maintained:
        # - Moved one node from unreversed to reversed
        # - All processed nodes are reversed and point to prev

    # Loop exit: current is None
    # prev points to new head (last original node)
    # All nodes reversed

    return prev

from threading import Lock

class Counter:
    def __init__(self):
        self.value = 0
        self.lock = Lock()

    def increment(self):
        with self.lock:
            self.value += 1

class Counter:
    """
    Thread-safe counter.

    Class Invariants:
        - value >= 0
        - lock is always valid
        - value reflects total increments

    Concurrency Properties:
        - increment is atomic
        - Multiple threads can safely call increment
        - No race conditions
        - Each increment increases value by exactly 1
    """

    def __init__(self) -> None:
        """
        Create new counter.

        Postconditions:
            - self.value == 0
            - self.lock is initialized
            - Thread-safe operations enabled
        """
        self.value = 0
        self.lock = Lock()

    def increment(self) -> None:
        """
        Atomically increment counter by 1.

        Preconditions:
            - Counter is initialized

        Postconditions:
            - self.value == old(self.value) + 1
            - Operation is atomic (thread-safe)

        Concurrency guarantees:
            - Mutual exclusion: Only one thread in critical section
            - Progress: Non-blocking (eventually acquires lock)
            - No deadlock: Lock always released
            - Visibility: Changes visible to all threads
        """
        with self.lock:
            # Critical section
            old_value = self.value
            self.value += 1
            # Postcondition: self.value == old_value + 1

def function_name(param1: Type1, param2: Type2) -> ReturnType:
    """
    [Brief description]

    :param param1: [Description]
    :param param2: [Description]
    :returns: [Description]
    :raises ExceptionType: [When]

    Preconditions:
        - [Condition on param1]
        - [Condition on param2]
        - [State requirement]

    Postconditions:
        - [Property of return value]
        - [State change]
        - [Side effect]
    """

class ClassName:
    """
    [Description]

    Class Invariants:
        - [Property 1 always true]
        - [Property 2 always true]
    """

    def __init__(self, ...):
        """
        Preconditions: [...]
        Postconditions: [Invariants established]
        """

    def method(self, ...):
        """
        Preconditions: [Invariants hold, ...]
        Postconditions: [Invariants still hold, ...]
        """

# Loop invariant:
# - [Property true at loop entry and after each iteration]
# - [Relates loop variable to progress]
# - [Relates accumulator to partial result]

while condition:
    # Invariant holds here

    # Loop body

    # Invariant maintained