icontract-hypothesis VS clang-contracts

https://github.com/mristin/icontract-hypothesis

Nagini and deal-solver attempt to Formally Verify Python code with or without unit tests: https://news.ycombinator.com/item?id=39139198

Additional research:

"Fuzz target generation using LLMs" (2023)

https://icontract.readthedocs.io/en/latest/usage.html#invari...

For unit testing, there's icontract-hypothesis; with the Preconditions and Postconditions delineated by e.g. decorators, it's possible to generate many of the fuzz tests from the additional Design by Contract structure of the source.

From https://github.com/mristin/icontract-hypothesis :

> icontract-hypothesis combines design-by-contract with automatic testing.

> It is an integration between icontract library for design-by-contract and Hypothesis library for property-based testing.

> The result is a powerful combination that allows you to automatically test your code. Instead of writing manually the Hypothesis search strategies for a function, icontract-hypothesis infers them based on the function’s [sic] precondition

Just in case you are looking for an alternative approach: if you write contracts in your code, you might also consider crosshair [1] or icontract-hypothesis [2]. If your function/method does not need any pre-conditions then the the type annotations can be directly used.

(I'm one of the authors of icontract-hypothesis.)

[1] https://github.com/pschanely/CrossHair

[2] https://github.com/mristin/icontract-hypothesis

I'm the author, and even I think so. I'm more of an LLVM fan myself (though I can't not mention David Malcom's work on the GCC Static Analyzer).

Ideally it wouldn't be a plugin at all, it'd be a language feature. We got Contracts and left out the most useful contract of them all, the stateful invariant!

Originally, I started it as a Clang plugin, thinking that I could also implement support for the Contracts "[[pre]]" and "[[post]]" specification on top (or at least some minimal implementation of it.

The difficulty seemed a lot greater to support pre/post attributes with expressions inside of them than [[invariant]] marker attributes.

If people would like to use this from Clang, even without support for regular Contracts, I will publish a compatible Clang plugin.

I think at some point there was support for Contracts in Clang, maybe longer term I'll try to get them working again? (I've no experience here)

https://github.com/arcosuc3m/clang-contracts

This fellow wrote a whole ~200 page thesis on this just as recently as 2018, such a shame for it to go to waste =/

https://e-archivo.uc3m.es/bitstream/handle/10016/29231/TFG_J...