deal

Deal is a Python library for Design by Contract (DbC) that provides several layers of verification:

• Core DbC: Support for preconditions, postconditions, and invariants.
• Side-effect & Exception Tracking: Ability to track exceptions and ensure functions are pure.
• Testing & Verification: Property-based testing, integration with hypothesis and pytest, and formal verification to prove code correctness.
• Static Analysis: A linter and integration with flake8 for static contract checking.
• Advanced Checks: Memory leak detection for pure functions and support for external validators.
• Production Ready: Zero-dependency runtime (dependencies are only for analysis tools) and the ability to enable/disable contracts in production.

Markers are properties of a function and are not conditional. If a function can perform a side-effect (e.g., inside an if branch), it must declare the corresponding marker regardless of whether that branch is actually executed during a specific call.

When using the Deal linter, a function will fail if it calls another function with a marker that the caller has not declared, even if the specific execution path that triggers the side-effect is not taken.

import deal

def run_job(job_name: str, silent: bool):
    if not silent:
        print('job started')

@deal.has()  # This will fail linter check because it misses 'stdout'
def main():
    job_name = 'hello'
    run_job(job_name, silent=True)
    return 0

Certain markers are enforced at runtime by patching standard library modules. If a function attempts a side-effect that is not declared via @deal.has, Deal will raise an exception:

• Network: If io, network, or socket is NOT specified, network requests are blocked. Attempting them raises OfflineContractError.
• Stdout: If io, print, or stdout is NOT specified, sys.stdout is patched. Attempting to use it raises SilentContractError.
• Stderr: If io or stdout is NOT specified, sys.stderr is patched similarly to stdout.

Note: Other markers are currently only checked by the linter and do not trigger runtime exceptions.

@deal.has()
def f():
    print('hello')

f()
# Raises SilentContractError:

To validate pre and post contracts, the linter performs partial execution of the contract logic. If a contract cannot be executed (e.g., due to complexity or side effects), the linter will silently ignore it.

To ensure your contracts are linter-friendly and detectable, follow these best practices:

• Avoid side-effects: Do not include logging or other state-changing operations within a contract.
• Avoid external dependencies: Do not rely on functions or constants defined outside of the contract scope.
• Keep contracts small: If you have multiple validation requirements, use separate contracts rather than one large one.

import deal

@deal.post(lambda r: r != 0)
def f():
    return 0

While standard if/else blocks can handle multiple logic paths, using @deal.dispatch provides several advantages for complex logic (e.g., handling different file formats or recursive algorithms):

1. Isolation: Each implementation is isolated, making the code easier to read and maintain.
2. Direct Access: Individual implementations can be called directly by users or in tests.
3. Guaranteed Correctness: Because preconditions are attached to the specific implementations, calling an implementation directly still ensures it is used correctly.
4. Extensibility: It provides a built-in plugin system, allowing users to register new implementations for the dispatched function.

Deal uses a JIT-like approach where heavy operations (like function and validator introspection) are performed only once, when the function is called for the first time.

To manage performance in benchmarks or production:

1. Disable contracts: Use deal.disable.
2. Trigger lazy caching: Call the function once in advance.
3. Pre-cache everything: Use deal.introspection.init_all to pre-cache contracts for all functions.

To avoid duplicating a function's signature (including default arguments) inside a contract, you can use a lambda or function that accepts a single _ argument. Deal will pass a container containing all function arguments (including defaults) to this argument.

@deal.pre(lambda _: _.a + _.b > 0)
def f(a, b=1):
    return a + b

@deal.pre(lambda _: _.a + _.b > 0)
def f(a, b=1):
    return a + b

f(1)
# 2

f(-2)
# PreContractError: expected a + b > 0 (where a=-2, b=1)

The formal verifier uses specific logical interpretations for Deal's contract decorators and assertions. It treats them as either given (axioms that must be satisfied by a counter-example) or expected (assertions that the theorem tries to break/violate).

In a simplified/short contract signature, the contract object (often named _) is a dict that allows attribute access. If one of your function arguments has the same name as a standard dictionary method (e.g., items), you cannot use dot notation (_.items). Instead, use getitem syntax to access the argument.

# If an argument is named 'items', use:
_['items']
# instead of
_.items

Deal operates under the open-world assumption. This means:

• Deal can identify when a contract violation occurs (e.g., if a function explicitly raises an exception or fails on a specific input).
• Deal cannot prove that a violation is impossible. If a function might fail deep in the call stack on a very rare input, Deal might not catch it.
• If you declare that a function can raise a specific exception (e.g., ValueError) but Deal does not observe it during its checks, Deal will trust your declaration rather than arguing that it's impossible.