Ada-like library contracts

[fenollp]

Hello Xavier!

I wish to continue the discussion about contract testing I think we started at the last meetup at Scaleway.

There's this way of specifying pre/post conditions centered around the usage of a library's functions in Ada/spark https://docs.adacore.com/spark2014-docs/html/ug/en/source/subprogram_contracts.html

I like how library creators can specify contracts on the functions they publish and their users then restrict these contracts and verify their usage of the lib.

To me this kind of dev experience is best. Buy in is split among lib writers and users which should lower the bar to entry.

How can one go with using creusot (or a sub project) and apply such contracts on a production project today?
I would like to bring formal methods to my team and I think Ada's approach would fit well with my managers and teammates.

Thanks!

[xldenis]

Hi,

Today, library authors can easily attach contracts to their public apis which will be picked up in client code compiled by creusot.
You can see examples of this increusot-contracts. Furthermore, clients can themselves provide contracts for library code through the extern_spec! mechanism.

Does that answer your question? I'd love to hear more about the kinds of contracts you would need / features you think you would use.