Contract stub files

[amacfie]

By analogy to type stub files maybe we'd want to be able to write contract stub files for third party libraries. They wouldn't be checked, they'd just be there to tell CrossHair facts to make its job easier.

[pschanely]

This is a great idea! I've done a tiny amount of thinking along these lines as well. There's a nice idea in there about what behaviors the library author is trying guarantee (and maybe what behaviors the author isn't). Perhaps we even recommend that contracts go directly into the pyi file, right along with the types! (I think all type checkers ignore the function bodies)

In addition, I think it would be really interesting to think about how contracts could change the way we think about library versioning: CrossHair could theoretically tell you whether your contract changes are backwards-compatible (i.e. it's safe to weaken your preconditions, or strengthen your postconditions).

[amacfie]

Is it possible to do this by putting code into the checked codebase that dynamically modifies docstrings or applies icontract decorators to functions in third party modules?

Addendum: Appending to mod.fn.__doc__ doesn't work because CrossHair only gets conditions that are actually there in the docstring source. And mod.fn = icontract.ensure(...)(mod.fn) doesn't work because CrossHair tries to stringify the contract and without an actual decorator this fails. In both cases it would be easy to change CrossHair's behavior to handle this usage.

[pschanely]

Ah, wow, you found the ugliness with __doc__ and source inspection: FWIW, this hoop-jumping is largely here to be able to report line numbers. It might not be super easy to unwind.

I think I'd consider trying to tackle this as an explicit part of the condition parsing.
All conditions are parsed through a relatively straightforward/composable interface: ConditionParser.

We might consider making a new kind of ConditionParser that wraps another ConditionParser. Not only would this parser look for conditions on the given runtime object, but it would also try to import the corresponding stub object (perhaps we import it under a new loplevel package name or something) and look for conditions on that as well. It would delegate all the actual work to the wrapped parser, so the icontract, pep316, and assert-based parsers would effectively work the same on the stub as the real object.

Note that if we did want to put contracts into the pyi files, we also need to think about @overloads. This is good, because we'd like to know about those signatures anyway (#46), but complicates the solution, and opens important/hard product questions about whether, for instance, you are expected to define contracts per-overload. Feels like it almost needs a "CrossHair PEP" or something :)

Perhaps to temper your enthusiasm just a little: the way in which CrossHair uses conditions of called functions is rather limited. Essentially, CrossHair may try to "skip" execution of the body, and use only the conditions to prove the outer condition holds. If successful, we know that we don't have to keep trying this path. If unsuccessful, however, we just keep trying, but by executing paths through the function body. This is a sort of tactic that can backfire - if the conditions on called function are commonly not sufficient to prove the caller's conditions, it's actually counterproductive to use them.

[pschanely]

A note: @lmontand is actively working on something that is approaching this request: a programmatic way to attach contracts to existing functions. We'll update this thread when there is something more concrete to say!