Re: Ada noob here! Is Ada widely used?

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Mon, 07 Jun 2010 13:13:18 +0200, Georg Bauhaus  
<rm.dash-bauhaus@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.