Date Range Validator

Build a date range validation utility with formal contract specifications. The implementation should include preconditions and postconditions that can be verified to ensure correctness.

Capabilities

Date Range Validation

Validates that a date falls within a specified range and performs date arithmetic correctly.

• Given start date "2024-01-01", end date "2024-12-31", and check date "2024-06-15", returns True @test
• Given start date "2024-01-01", end date "2024-12-31", and check date "2025-01-01", returns False @test
• Given start date "2024-01-01", end date "2024-01-31", adding 15 days to start date results in "2024-01-16" @test

Business Day Calculation

Calculates the number of days between two dates and validates business logic constraints.

• Given start date "2024-01-01" and end date "2024-01-10", returns 9 days difference @test
• Given start date "2024-01-01" and end date "2024-01-01", returns 0 days difference @test

Implementation

@generates

API

from datetime import date, timedelta

def is_date_in_range(start: date, end: date, check: date) -> bool:
    """
    Check if a date falls within a specified range (inclusive).

    pre: start <= end
    post: __return__ == (start <= check <= end)
    """
    pass

def add_days_to_date(start: date, days: int) -> date:
    """
    Add a specified number of days to a date.

    pre: days >= 0
    post[start]: __return__ >= start
    """
    pass

def days_between(start: date, end: date) -> int:
    """
    Calculate the number of days between two dates.

    pre: start <= end
    post: __return__ >= 0
    """
    pass

Dependencies { .dependencies }

crosshair-tool { .dependency }

Provides symbolic execution and contract verification capabilities for Python code, including support for standard library types like datetime.

@satisfied-by