Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Ada for the C++ and Java Developer [pdf]

learn.adacore.com

Post reply on HN
Print view View original

51–60 of 72 posts

Re: Ada for the C++ and Java Developer [pdf]

#51

Post by nerdponx »

twoodfin wrote: post #42
thesuperbigfrog wrote: post #38

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 o…

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…

Is it not possible to use refinement types to erase some (but maybe not all) runtime checks but still maintain a type safety guarantee?

Re: Ada for the C++ and Java Developer [pdf]

#53

Post by beached_whale »

pjmlp wrote: post #44
thesuperbigfrog wrote: post #38

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 o…

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/pap…

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

Re: Ada for the C++ and Java Developer [pdf]

#54

Post by agumonkey »

thesuperbigfrog wrote: post #38

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 o…

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

Re: Ada for the C++ and Java Developer [pdf]

#55

Post by Jtsummers »

agumonkey wrote: post #54
thesuperbigfrog wrote: post #38

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 o…

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

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.

Re: Ada for the C++ and Java Developer [pdf]

#56

Post by boibombeiro »

agumonkey wrote: post #54
thesuperbigfrog wrote: post #38

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 o…

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

You can use formal verification tools to verify the code. Having preconditions ("assume" instead of "assert") reduces the search space.

Re: Ada for the C++ and Java Developer [pdf]

#57

Post by vram22 »

thesuperbigfrog wrote: post #38

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 o…

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.

Re: Ada for the C++ and Java Developer [pdf]

#58

Post by csb6 »

twoodfin wrote: post #42
thesuperbigfrog wrote: post #38

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 o…

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…

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.

Re: Ada for the C++ and Java Developer [pdf]

#59

Post by rramadass »

twoodfin wrote: post #42
thesuperbigfrog wrote: post #38

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 o…

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…

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.

Re: Ada for the C++ and Java Developer [pdf]

#60

Post by rramadass »

agumonkey wrote: post #54
thesuperbigfrog wrote: post #38

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 o…

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

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.

Post reply on HN