Re: Silly and stupid post-condition or not ?

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

Le Sat, 04 Feb 2012 04:16:34 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:
> But to claim that just because it's practically impossible to describe  
> the complete behavior of real systems does not mean that there is no  
> benefit to describing the easy part. And that is exactly what you are  
> arguing -- and it should be clear to any Ada programmer that that is a  
> fallicy.
At least an Ada practice was always there, even far prior it integrated  
DbC™: express as much validity constraints as you can with the type system.

The type system cannot express every constraint (and that's clear to  
everyone), but it still useful. The same with DbC. Moreover, with DbC, you  
may indeed have to care about efficiency. Anyway, if one want very strict  
proof and cases coverage, there are other tools or languages: SPARK & Cie.  
There is no way to impose such things to every application and every Ada  
source author. On the opposite, this would even prevent authors from  
keeping Ada in mind as an option.

98% is not 100%, but better what you can really and practically get than  
any promise you will not ever access to, and which will turn a something  
far below 98% or to simply nothing.

Time to recall safety and proof level is not to be the same for every Ada  
applications, and to recall this level is to be defined by the  
application's specifications. No need to design an application outside of  
its specifications (except as a game, challenge or other experiments).

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University