User Account Manager

A user account management system that validates user operations using runtime contract enforcement.

Capabilities

Account creation validation

• Creating a user with valid username (alphanumeric, 3-20 chars) and age (18-120) succeeds @test
• Creating a user with username shorter than 3 characters raises PreconditionFailed @test
• Creating a user with age below 18 raises PreconditionFailed @test
• Creating a user with age above 120 raises PreconditionFailed @test

Account balance operations

• Depositing a positive amount to an account increases the balance by that amount @test
• Depositing a negative or zero amount raises PreconditionFailed @test
• Withdrawing an amount less than or equal to balance succeeds and decreases balance @test
• Withdrawing an amount greater than balance raises PreconditionFailed @test
• Withdrawing ensures balance never becomes negative @test

Username updates

• Updating username to a valid name (alphanumeric, 3-20 chars) succeeds @test
• Updating username to an invalid name raises PreconditionFailed @test

Implementation

@generates

API

class UserAccount:
    """
    A user account with username, age, and balance.

    Attributes:
        username: Alphanumeric string, 3-20 characters
        age: Integer between 18 and 120 (inclusive)
        balance: Non-negative float
    """

    def __init__(self, username: str, age: int) -> None:
        """
        Create a new user account.

        Args:
            username: The username for the account
            age: The user's age
        """
        pass

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

        Args:
            amount: The amount to deposit
        """
        pass

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

        Args:
            amount: The amount to withdraw
        """
        pass

    def update_username(self, new_username: str) -> None:
        """
        Update the account's username.

        Args:
            new_username: The new username
        """
        pass

Dependencies { .dependencies }

crosshair-tool { .dependency }

Provides runtime contract enforcement with decorators for validating preconditions and postconditions.