What's the most widely-used open source project that uses design by contract?

Question

I'm curious about how much design-by-contract is used in practice outside of the Eiffel community. Are there any active open-source projects that use design-by-contract?

Or, to recast the question into one what that has a single answer: what's the most widely-used (non-Eiffel) open-source project that uses design-by-contract?

Answer 1

The "non-Eiffel" part of your question is interesting. Contracts take all their sense when there is support for them in the programming language, otherwise it's just a nice syntax for comments.

That brings us to the languages that support contracts. I know of three except Eiffel:

• ESC/Java adds contracts to Java using a language named JML.
• .NET contracts for all .NET languages (works at the bytecode level)
• Frama-C adds contracts to C using the language ACSL

The first two have executable contracts. Advantages: can be used as run-time assertions. Disadvantages: lack the expressive power to completely specify what a function does in a contract. You can basically only write sanity checks.

ACSL contracts on the other hand are more expressive, and not executable. They make it possible to completely specify that a sort function should always terminate, and leave the same elements as in the original array in order. ACSL contracts can be used for static analysis, especially Hoare-style weakest precondition computation.

And only being really familiar with the last one (disclaimer: I work on Frama-C, but the ACSL part is the work of a lot of people, some of whom have contributed much more than me), I can only mention "ACSL by example", an open source C library with ACSL contracts currently being developed by Fraunhofer FIRST. It's not released yet, but it will be as part of the Device-soft project. I am sure that you could get a preliminary version if you were interested. Feel free to contact the person mentioned as contact on that last web page.