Bank Account Manager

Build a simple bank account manager that validates account operations using contract-based verification. The system should enforce business rules through preconditions and postconditions to ensure valid account transactions.

Requirements

Implement a BankAccount class that manages account balance and transactions with the following operations:

Account Creation

• Create accounts with an initial balance (must be non-negative)
• Each account has an account number (string) and balance (float)

Deposit Operations

• Deposits must be positive amounts
• The balance should increase by the deposit amount after a successful deposit
• Return the new balance after deposit

Withdrawal Operations

• Withdrawals must be positive amounts
• Cannot withdraw more than the current balance (no overdrafts)
• The balance should decrease by the withdrawal amount after a successful withdrawal
• Return the new balance after withdrawal

Balance Inquiry

• Provide a method to get the current balance
• Balance must always be non-negative

Transfer Operations

• Transfer money from one account to another
• Transfer amount must be positive
• Source account must have sufficient funds
• After transfer, source balance decreases and destination balance increases by the transfer amount

Validation Requirements

The implementation must use contract-based specifications to enforce these business rules. You should define:

• Preconditions: Validate inputs before operations execute
• Postconditions: Verify correct state changes after operations complete
• Class Invariants: Ensure balance is never negative throughout the object's lifetime

You may use any contract specification approach, including:

• Docstring-based contracts
• Decorator-based contracts
• Assertion-based validation
• Or any combination of approaches

Test Cases

Implement the following test cases:

• Basic deposit increases balance correctly @test
• Withdrawal with sufficient funds succeeds @test
• Withdrawal exceeding balance is rejected @test
• Transfer between accounts works correctly @test
• Negative deposit amount is rejected @test

Implementation

@generates

API

class BankAccount:
    """
    A bank account that enforces business rules through contract verification.
    """

    def __init__(self, account_number: str, initial_balance: float) -> None:
        """
        Initialize a bank account with an account number and initial balance.

        Args:
            account_number: Unique identifier for the account
            initial_balance: Starting balance (must be non-negative)
        """
        pass

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

        Args:
            amount: Amount to deposit (must be positive)

        Returns:
            New balance after deposit
        """
        pass

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

        Args:
            amount: Amount to withdraw (must be positive and <= balance)

        Returns:
            New balance after withdrawal
        """
        pass

    def get_balance(self) -> float:
        """
        Get the current account balance.

        Returns:
            Current balance
        """
        pass

    def transfer(self, amount: float, destination: 'BankAccount') -> None:
        """
        Transfer money to another account.

        Args:
            amount: Amount to transfer (must be positive and <= balance)
            destination: The destination account
        """
        pass

Dependencies { .dependencies }

crosshair-tool { .dependency }

Provides contract verification and symbolic execution capabilities for Python code.