Contract Patterns Corpus

[kde-baskets-user]

Hello,

I’ve just started my journey with CrossHair. First of all, I’d like to thank you; this is quite impressive work!

I have a few beginner questions. Perhaps it’s covered somewhere, but what I’ve missed is a corpus of typical scenarios: typical problems, possible solutions, and discussions for each scenario. I am still looking into python-by-contract-corpus; perhaps it will do, but at first glance, it's not it though.

More precisely, I’d like to see:

• Domination/Post-Domination Contracts: How to ensure that code X always executes before/after code Y, for any possible code path?
• Global State Contracts: How to express contracts related to global state, such as ensuring that no new listeners are added to some object after its initial configuration is completed, i.e. certain operations are permitted only in certain life cycle phases?
• Expired Value Contracts: In a producer-consumer model, when the producer repeatedly sends values to a consumer, how to guarantee that the consumer always receives a fresh value from the current round/transaction, in other words, that it’s not expired?
• Lost Update Contracts: In the same producer-consumer model, how to detect situations where a produced value was not consumed in the current round. i.e. lost?

Apart from this, I am willing to invest some time to learn the internals and possibly contribute. However, for several years now, I haven’t worked with just a single language. Nowadays, projects are a mix of different tools, and in my case, it’s a C/C++/Python codebase mostly with a gradual shift to Rust. Notably, Klee (a verification platform for C/C++) also uses Z3 internally. With that in mind, perhaps there’s a common level that these various platforms can reuse and benefit from, some shared intefaces. What do you think?

[pschanely]

Wow. There are a lot of interesting ideas in here! Some of my reactions:

• You aren't mistaken: there is nothing in the CrossHair docs that really walks you through typical scenarios, or gives you an idea about how or when to apply it. You can find some resources that are applicable but not CrossHair-specific, e.g.:
  • https://icontract.readthedocs.io/en/latest/recipes.html (crosshair can check icontract contracts too)
  • https://www.hillelwayne.com/post/contract-examples/ (property based testing is very closely related to contract testing - and you can always write a standalone function with a contract to make a property-based test)
• Most of your specific examples have an imperative flavor; I think a typical answer is to transform the challenge into a more functional framing, and combine that with the trick I just mentioned about writing property-based tests:
  • To determine code X runs before code Y, append checkpoints for having run X and Y to a list and return that. Then your contract says that a Y checkpoint doesn't occur before an X checkpoint.
  • For global state, you could initialize the global state to a symbolic value provided by the test, and then return the global state after running the code you want to test. Of course, avoiding global state in the first place is probably better.
  • Producer/consumer problems might be framed as a property test where you process a list of input messages, and assert something about the list of output messages.
• Shared interfaces across languages: there might be an interesting opportunity here! Perhaps this is introducing a contract specification language for JSON-RPC, GraphQL, etc.
• As far as contributing goes, it feel like most of the topics you're talking about might be more in the documentation/tutorial zone, but I'd be curious about what ideas you might have for improving the tooling as well. (perhaps we should implement an analog to Hypothesis's stateful testing mode?) I'd be happy to collaborate on an official CrossHair tutorial, but also if you wanted to just write your own (and it's good!), I'd also be happy to prominently link it from the CrossHair docs.