interactive query mode

[amacfie]

Say I'm in ptpython and I import a function f. (Maybe f has a contract, maybe it doesn't.) What I'd like to do is run a few lines of python code to create a precondition-postcondition pair and ask CrossHair whether f satisfies it. Currently to do this I'd have to create a new scratch file, write a wrapper function for f with the exact same signature, add a contract, and run CrossHair maybe with the watch command.

[pschanely]

I like this thought. (and generally, the idea about how symbolic stuff could help the REPL) Opinions about the interface?

>>> crosshair.watch(parse_int_fn, post = lambda _: _ != 42)
Exploring paths, Ctrl-C to stop: .............. counterexample found:
BoundArguments(x="42")
>>> 

Related, occasionally someone expresses an interest in invoking crosshair programmatically.

There are some practical issues, but I think they are resolvable. At least currently, CrossHair causes some permanent brain damage to its host interpreter. The native datetime and json libraries currently get swapped with pure-python versions, for example. We'd also want to circumvent the auditwall stuff, because IIRC sys.addaudithook() is not undo-able. There is a likely another gotcha or two that I'm not recalling at the moment.

[amacfie]

crosshair.check not crosshair.watch right?

[pschanely]

crosshair.check not crosshair.watch right?

Ah. I think I reached for the watch name just because this incarnation wouldn't have a timeout by default. But obviously it couldn't "watch" the code for changes or anything. Indeed check is probably much less confusing. Or we name it something else entirely.