(option to) Treat leading assertions as preconditions about crosshair HOT 7 CLOSED

I am warming up to this request generally. And, FWIW, I think some sort of hypothesis cooperation also makes a lot of sense.

In the assert version, do you imagine pulling the AST, and making the assumption that the first non-assert statement in the body signals the transition from preconditions to postconditions?

from crosshair.

@Zac-HD This is in-progress :)

In other modes, CrossHair detects other kinds of exceptions too. I'm thinking this is useful under "assert mode" as well.

One notable exception might be ValueError & TypeError which are likely validating inputs? Or perhaps any exception raised directly in the body of the function under analysis? WDYT?

from crosshair.

A basic version of this is in HEAD! (minimalistic docs)

At least one leading assert is required, and it'll complain about any kind of exception.

There are no flags/options to control the behavior yet; I think I'm inclined to wait for feedback from real use cases? Another option for exception handling would be to borrow just the raises: <exception type> pattern from the docstring parser for suppressing exception reports.

from crosshair.

Docstring directives like "raises: IndexError" should work.
Complete docs for assert mode are here now.
Closing this FR!

from crosshair.

An alternative would be to special-case a function called assume, which might be implemented as

def assume(predicate):
    assert predicate

and treat assume(x) as expressing a precondition of bool(x) is True rather than an assertion. This would also play nicely with the hypothesis.assume() function, which does exactly this (albeit implemented with a special exception type). Other projects could add domain-specific logic such as logging that the precondition was violated or attempting to recover to a known-good state.

from crosshair.

In the assert version, do you imagine pulling the AST, and making the assumption that the first non-assert statement in the body signals the transition from preconditions to postconditions?

Exactly, though it should probably be configurable at the project level and also have some local way to force all-assertions-are-invariants.

from crosshair.

One notable exception might be ValueError & TypeError which are likely validating inputs? Or perhaps any exception raised directly in the body of the function under analysis? WDYT?

Maybe as a separate flag - I think this is probably useful, but also prone to concealing real bugs in a way that assertions-only is not.

from crosshair.