Checking multiple partial contracts

[andrew222651]

An idea that blurs the line between contracts and unit tests:

def f(x: float, y: float) -> float:
    '''
    This is the function that actually computes the value. It has no contract
    because a contract (return value non-negative) would short-circuit contract
    checking on cases below.

    The polynomial is the sum of squares
    (x y^2 - x + 3x^2)^2 + (x y - 3 + x^2 y^2 + x y^2)^2.
    '''
    return (x**4 * y**4 + 9 * x**4 + 2 * x**3 * y**4 + 2*x**3 * y**3
        + 6 * x**3 * y**2 - 6 * x**3 + 2 * x**2 * y**4 + 2 * x**2 * y**3
        - 7 * x**2 * y**2 + x**2 - 6 * x * y**2 - 6*x*y + 9)

def __crosshair_case_total(x: float, y: float) -> float:
    '''
    a normal contract for the function. not completely verifiable w/ CrossHair.

    post: __return__ >= 0
    '''
    return f(x, y)

def __crosshair_case_x0(y: float) -> float:
    '''
    some inputs are set, others are left for the contract fuzzer. verifiable.
    post: __return__ >= 0
    '''
    # this poly is constant
    return f(0, y)

def __crosshair_case_x1(y: float) -> float:
    '''
    also verifiable by CrossHair.
    post: __return__ >= 0
    '''
    # this poly has degree 4
    return f(1, y)

def __crosshair_case_x2y2() -> float:
    '''
    all inputs are set, i.e. a test
    post: __return__ >= 0
    '''
    return f(2, 2)

Alternatively, put test cases in an if statement in the precondition and
postcondition and then contract is public and CrossHair can use the contract for "short-circuiting" contract checking for callers:

def checkf(x: int, r: int) -> bool:
    if x == -2:
        return r == 2
    elif x >= 0:
        return r == x
    else:
        return r == -x

def f(x: int) -> int:
    '''
    pre: x == -2 or True
    post[]: checkf(x, __return__)
    '''
    return abs(x)

[pschanely]

These are some really nice examples!

For what it's worth, this is often the way I use CrossHair! I write little standalone functions with contracts that are essentially just property-based tests.

This also reminds me that it's about time to rethink some of how the short-circuiting mechanism is designed. Ideally, the square bracket thing would just be about immutability and not ALSO be a flag for CrossHair techniques like this. 😅