4 ms·

One of my favorite features of Ada 2012 are the design-by-contract checks taken from Eiffel[0]: Preconditions: "a condition or predicate that must always be t

One of my favorite features of Ada 2012 are the design-by-contract checks taken from Eiffel[0]: Preconditions: "a condition or predicate that must always be true just prior to the execution of some section of code or before an operation"[1]. It is up to the caller (client) to set up the preconditions and ensure that they are true before calling the code in question. If any preconditions are not met, it is the fault of the caller (client). Postconditions: "a condition or predicate that must always be true just after the execution of some section of code or after an operation"[2]. The code in question guarantees that the postconditions will be true after the code is executed. If any postconditions are not met, it is the fault of the callee (supplier). Invariants: conditions or predicates that "can be relied upon to be true during the execution of a program, or during some portion of it"[3]. Both parties must ensure the invariants hold. These features make it very easy to determine where a bug is in the code and make it very explicit what is expected of the caller (client) and callee (supplier). They act as run-time sanity checks and push Ada / SPARK code in the direction of Haskell function signatures and types. With proper preconditions, postconditions, and invariants in place I think it should be possible to implement a QuickCheck-style[4] testing system to provide some empirical checks if SPARK proof checking is not used. I would love to see these design-by-contact features added to Rust, C++, and even C. [0] https://www.eiffel.com/values/design-by-contract/introduction/ https://www.eiffel.com/values/design-by-contract/introductio... [1] https://en.wikipedia.org/wiki/Precondition https://en.wikipedia.org/wiki/Precondition [2] https://en.wikipedia.org/wiki/Postcondition https://en.wikipedia.org/wiki/Postcondition [3] https://en.wikipedia.org/wiki/Invariant_(mathematics)#Invariants_in_computer_science https://en.wikipedia.org/wiki/Invariant_(mathematics)#Invari... [4] https://en.wikipedia.org/wiki/QuickCheck https://en.wikipedia.org/wiki/QuickCheck

twoodfin 6y ago
The problem I’ve seen with trying to add non-static contracts to performance-sensitive languages has been ideological rather than technical. Specifically, do the language semantics allow a mode where these checks can be turned off? Leaving them on all the time can be a huge performance burden, both directly and in the barriers they add to optimization (while there are potential optimization benefits to exploiting the guarantees of contracts, I don’t think as a practical matter they balance out). But allowing them to be turned off in “release mode” eliminates much of the benefit in all modes: Developers can no longer assume that their code always runs in a context where the contractual guarantees are met, so they have to guard data integrity or safety critical operations dynamically anyway.
- touisteur 6y ago
  I guess it's as bounds check and other runtime validity checks integrated in the language. When we upgrade compiler versions, I usually run a global app profile (perf, and internal tools you must have when latency and cpu load are actual product requirements. Every 'new' hot spot is analyzed and if it's a contract, I check whether there's a less costly way to perform it, or if watering down the contract seems OK (usually not). The thing is, a precondition (especially if you went through AoRTE, or silver-level SPARK) can authorize you to aggressively remove all runtime checks (and get far more performant code) 'behind'.
- nerdponx 6y ago
  Is it not possible to use refinement types to erase some (but maybe not all) runtime checks but still maintain a type safety guarantee?
- csb6 6y ago
  They can be turned off for release mode, and the SPARK subset of Ada can use them in formal verification, proving that the conditions hold true for all inputs statically, eliminating the need for any checks. I think the performance impacts are usually not as big as you think (the Ada compiler is smart enough to eliminate redundant checks where it can), and I believe that they can be turned off per package, too, so for performance critical modules they can be deactivated in release mode. I do not think contracts were intended to raise recoverable errors in a normal application's behavior; if they are triggered, then the program is incorrect, not just encountering an error. I think most developers would leave them on in release mode (if possible) just to get stack traces and exception messages to see what failed.
- rramadass 6y ago
  The paper "Applying Design by Contract" by Bertrand Meyer shows how DbC is to be used. It is sufficient to have only preconditions turned on by default in "release" mode, others are optional. My thumb rule is to have all preconditions/postconditions/invariants turned on only in the boundary functions (i.e. public api) of a module while the inner cohesive functions only have preconditions turned on.
- 6y ago
pjmlp 6y ago
C++20 was supposed to have them, but they were removed on the very last minute, if we are lucky maybe C++23 will get them, but C++26 is most likely, if they ever go forward with them. [1] For C you can have a look at Frama-C. [2] D also has DbC. [3] In case you can target Windows only, VC++ supports SAL Annotations, while not DbC they help to improve code security [1] - http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2021/p2339r0.html http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2021/p233... [2] - https://frama-c.com/html/acsl.html https://frama-c.com/html/acsl.html [3] - https://dlang.org/spec/contracts.html https://dlang.org/spec/contracts.html [4] - https://docs.microsoft.com/en-us/cpp/code-quality/using-sal-annotations-to-reduce-c-cpp-code-defects?view=msvc-160 https://docs.microsoft.com/en-us/cpp/code-quality/using-sal-...
- beached_whale 6y ago
  One thing I am excited about is that we should be able to exploit the contracts in some circumstances to better performance.
agumonkey 6y ago
I never understood how is that different from decorating your function with `assert` statements. Is it analyzed statically ?
- Jtsummers 6y ago
  Yes. SPARK/Ada will attempt to verify many of the properties statically. Not everything can be, and not everything can be done without significant effort (that is, more than it may be worth). But it's more than asserts in most other languages which are only verifiable dynamically. For those areas where SPARK can't prove something statically, the checks are used at runtime (like a traditional assert). It's a best of both worlds situation, in that regard.
- boibombeiro 6y ago
  You can use formal verification tools to verify the code. Having preconditions ("assume" instead of "assert") reduces the search space.
- rramadass 6y ago
  asserts are just a language mechanism using which you implement preconditions/postconditions/invariants which are program correctness design constructs. Thus it is a systematic (i.e. not ad-hoc) way of using asserts correctly to guarantee program state. I highly recommend reading Bertrand Meyer's papers "Applying Design By Contract" and "Design by Contract". They are well worth every programmer's time.
vram22 6y ago
Any language that has assertions can be used to simulate at least preconditions and postconditions, and maybe some support for invariants. As the team leader for the second version of a database middleware product developed in C, being convinced by study of the efficacy of assertions for DbC and hence better quality software, I made sure my team used C assertions heavily throughout the codebase, at the entry and exit points of functions, to implement preconditions and postconditions, despite some opposition to it. End result: the product was a success, and was used in multiple software projects for customers. We were rewarded well for it. Edit: I first learned about DbC myself, via reading about Eiffel and Bertrand Meyer's work, early on.
- vram22 6y ago
  I should add that the product being a success wss not solely due to using assertions for DbC, of course, although, IMO, that did play a significant role in bug detection and hence removal and better product quality. I also ensured that the team consistently applied some other basic software engineering practices, which were not ordinarily followed in that company. The product success was the result of all the practices that were applied and also a good team.

twoodfin 6y ago

The problem I’ve seen with trying to add non-static contracts to performance-sensitive languages has been ideological rather than technical. Specifically, do the language semantics allow a mode where these checks can be turned off? Leaving them on all the time can be a huge performance burden, both directly and in the barriers they add to optimization (while there are potential optimization benefits to exploiting the guarantees of contracts, I don’t think as a practical matter they balance out). But allowing them to be turned off in “release mode” eliminates much of the benefit in all modes: Developers can no longer assume that their code always runs in a context where the contractual guarantees are met, so they have to guard data integrity or safety critical operations dynamically anyway.

touisteur 6y ago
I guess it's as bounds check and other runtime validity checks integrated in the language. When we upgrade compiler versions, I usually run a global app profile (perf, and internal tools you must have when latency and cpu load are actual product requirements. Every 'new' hot spot is analyzed and if it's a contract, I check whether there's a less costly way to perform it, or if watering down the contract seems OK (usually not). The thing is, a precondition (especially if you went through AoRTE, or silver-level SPARK) can authorize you to aggressively remove all runtime checks (and get far more performant code) 'behind'.
nerdponx 6y ago
Is it not possible to use refinement types to erase some (but maybe not all) runtime checks but still maintain a type safety guarantee?
csb6 6y ago
They can be turned off for release mode, and the SPARK subset of Ada can use them in formal verification, proving that the conditions hold true for all inputs statically, eliminating the need for any checks. I think the performance impacts are usually not as big as you think (the Ada compiler is smart enough to eliminate redundant checks where it can), and I believe that they can be turned off per package, too, so for performance critical modules they can be deactivated in release mode. I do not think contracts were intended to raise recoverable errors in a normal application's behavior; if they are triggered, then the program is incorrect, not just encountering an error. I think most developers would leave them on in release mode (if possible) just to get stack traces and exception messages to see what failed.
rramadass 6y ago
The paper "Applying Design by Contract" by Bertrand Meyer shows how DbC is to be used. It is sufficient to have only preconditions turned on by default in "release" mode, others are optional. My thumb rule is to have all preconditions/postconditions/invariants turned on only in the boundary functions (i.e. public api) of a module while the inner cohesive functions only have preconditions turned on.
6y ago

pjmlp 6y ago

C++20 was supposed to have them, but they were removed on the very last minute, if we are lucky maybe C++23 will get them, but C++26 is most likely, if they ever go forward with them. [1] For C you can have a look at Frama-C. [2] D also has DbC. [3] In case you can target Windows only, VC++ supports SAL Annotations, while not DbC they help to improve code security [1] - http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2021/p2339r0.html http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2021/p233... [2] - https://frama-c.com/html/acsl.html https://frama-c.com/html/acsl.html [3] - https://dlang.org/spec/contracts.html https://dlang.org/spec/contracts.html [4] - https://docs.microsoft.com/en-us/cpp/code-quality/using-sal-annotations-to-reduce-c-cpp-code-defects?view=msvc-160 https://docs.microsoft.com/en-us/cpp/code-quality/using-sal-...

beached_whale 6y ago
One thing I am excited about is that we should be able to exploit the contracts in some circumstances to better performance.

agumonkey 6y ago

I never understood how is that different from decorating your function with `assert` statements. Is it analyzed statically ?

Jtsummers 6y ago
Yes. SPARK/Ada will attempt to verify many of the properties statically. Not everything can be, and not everything can be done without significant effort (that is, more than it may be worth). But it's more than asserts in most other languages which are only verifiable dynamically. For those areas where SPARK can't prove something statically, the checks are used at runtime (like a traditional assert). It's a best of both worlds situation, in that regard.
boibombeiro 6y ago
You can use formal verification tools to verify the code. Having preconditions ("assume" instead of "assert") reduces the search space.
rramadass 6y ago
asserts are just a language mechanism using which you implement preconditions/postconditions/invariants which are program correctness design constructs. Thus it is a systematic (i.e. not ad-hoc) way of using asserts correctly to guarantee program state. I highly recommend reading Bertrand Meyer's papers "Applying Design By Contract" and "Design by Contract". They are well worth every programmer's time.

vram22 6y ago

Any language that has assertions can be used to simulate at least preconditions and postconditions, and maybe some support for invariants. As the team leader for the second version of a database middleware product developed in C, being convinced by study of the efficacy of assertions for DbC and hence better quality software, I made sure my team used C assertions heavily throughout the codebase, at the entry and exit points of functions, to implement preconditions and postconditions, despite some opposition to it. End result: the product was a success, and was used in multiple software projects for customers. We were rewarded well for it. Edit: I first learned about DbC myself, via reading about Eiffel and Bertrand Meyer's work, early on.

vram22 6y ago
I should add that the product being a success wss not solely due to using assertions for DbC, of course, although, IMO, that did play a significant role in bug detection and hence removal and better product quality. I also ensured that the team consistently applied some other basic software engineering practices, which were not ordinarily followed in that company. The product success was the result of all the practices that were applied and also a good team.