Ada noob here! Is Ada widely used?
in [ADA]
|
Prev: Symbolic tracebacks on Debian (Was: About static libraries and Debian policy)
Next: Gnat cross compiler
From: Yannick Duchêne (Hibou57) on 7 Jun 2010 08:56 Le Mon, 07 Jun 2010 13:13:18 +0200, Georg Bauhaus <rm.dash-bauhaus(a)futureapps.de> a écrit: > DbC, however, has to do with designing components of the ship. > You can have rescue clauses (exception handlers) > in DbC. Yes, DnC is rather part of design than part of the application. This may not be perfect (words to Dmitry), while this still help to focus on design. BTW, nobody claimed DbC as proposed for Ada 2012 was sufficient to prove a program. Ada also has an expected role in pedagogy, and DbC can help it to play this role. I believe this way of DbC is most likely to attract people than a more strict one (two teachers here said even students tend to avoid designing... so try to figure what the crowd's behavior can be) like SPARK (which is neither perfect for some practical reasons although it perfectly sounds). The important fact is that it is a step toward without any step backward. I neither believe the proposed DbC will ever bloat Ada or give it any weakness holes. I agree with you (still talking to Dmitry), when you complain, as an example, generics comes with numerous troubles ; however, if a comparison was to be made, we will probably see Ada's DbC will comes with far less troubles (in the program proof area) than generics which are already there from long. There is no reason to focus on Ada 2012 DbC as a potential source of trouble. May be an opportunity to ask (a second time) for a question I have in mind: will SPARK (in the future) get benefit from Ada's DbC annotations ? -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.
From: Yannick Duchêne (Hibou57) on 7 Jun 2010 08:58 Le Sun, 06 Jun 2010 15:10:48 +0200, Dmitry A. Kazakov <mailbox(a)dmitry-kazakov.de> a écrit: > To put a hand grenade in your pocket, is safer than in the mouth... This picture has no foundation to me (an arbitrary picture which does not represent any relevant measurements of what the reality is) -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.
From: Dmitry A. Kazakov on 7 Jun 2010 09:20 On Mon, 07 Jun 2010 14:58:37 +0200, Yannick Duch�ne (Hibou57) wrote: > Le Sun, 06 Jun 2010 15:10:48 +0200, Dmitry A. Kazakov > <mailbox(a)dmitry-kazakov.de> a �crit: >> To put a hand grenade in your pocket, is safer than in the mouth... > This picture has no foundation to me (an arbitrary picture which does not > represent any relevant measurements of what the reality is) It illustrates meaningless of comparisons like "safer" taken out of context. Maybe better one would be: NASA trained astronauts to climb trees, because being on a tree you would be closer to the Moon. Identifiers as goto labels in Ada are safer than numeric labels in FORTRAN. Did that make gotos better? Yes, it did. Does that justify use of gotos? By no means. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Dmitry A. Kazakov on 7 Jun 2010 09:27 On Mon, 07 Jun 2010 14:56:54 +0200, Yannick Duch�ne (Hibou57) wrote: > Le Mon, 07 Jun 2010 13:13:18 +0200, Georg Bauhaus > <rm.dash-bauhaus(a)futureapps.de> a �crit: >> DbC, however, has to do with designing components of the ship. >> You can have rescue clauses (exception handlers) >> in DbC. > Yes, DnC is rather part of design than part of the application. > > This may not be perfect (words to Dmitry), while this still help to focus > on design. I fail to see how misleading stuff may focus on design. Executable contracts is just rubbish. They will rather distract from design in favor debugging. Ada was designed as a language of little or no debugging. Unfortunately it rapidly loses the ground. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 7 Jun 2010 10:09
On 07.06.10 15:27, Dmitry A. Kazakov wrote: > On Mon, 07 Jun 2010 14:56:54 +0200, Yannick Duch�ne (Hibou57) wrote: > >> Le Mon, 07 Jun 2010 13:13:18 +0200, Georg Bauhaus >> <rm.dash-bauhaus(a)futureapps.de> a �crit: >>> DbC, however, has to do with designing components of the ship. >>> You can have rescue clauses (exception handlers) >>> in DbC. >> Yes, DnC is rather part of design than part of the application. >> >> This may not be perfect (words to Dmitry), while this still help to focus >> on design. > > I fail to see how misleading stuff may focus on design. Executable > contracts is just rubbish. Not all DbC contracts need to be executable. Their being executalbe is considered accidental, not essential; Ada's aspect notation would not currently support this, though, IIUC. > They will rather distract from design in favor > debugging. We'll see. I still wonder why one would not want to specify more than the subtype constraints can achieve (without contorted(?) emulation of another type system). |