From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,ea5071f634c2ea8b X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.0.170 with SMTP id 10mr4528043pbf.2.1322059347824; Wed, 23 Nov 2011 06:42:27 -0800 (PST) Path: lh20ni9319pbb.0!nntp.google.com!news1.google.com!news3.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!87.79.20.101.MISMATCH!newsreader4.netcologne.de!news.netcologne.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 23 Nov 2011 15:42:25 +0100 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:8.0) Gecko/20111105 Thunderbird/8.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug. References: <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.com> <4295dc09-43de-4557-a095-fc108359f27f@y42g2000yqh.googlegroups.com> <3snehoqgs8ia$.1nobjem6g6hx6$.dlg@40tude.net> <128rdz2581345$.c4td19l7qp9z$.dlg@40tude.net> <16ipwvpdavifr$.17bxf7if7f6kh$.dlg@40tude.net> <4ecb78b1$0$6643$9b4e6d93@newsspool2.arcor-online.net> <1iofgbqznsviu$.phvidtvxlyj4$.dlg@40tude.net> <4ecbb96e$0$6581$9b4e6d93@newsspool3.arcor-online.net> <4ecbdfdb$0$6629$9b4e6d93@newsspool2.arcor-online.net> <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net> <4ecc35b8$0$7628$9b4e6d93@newsspool1.arcor-online.net> <4eccd5d2$0$6637$9b4e6d93@newsspool2.arcor-online.net> <14p8llstxrtci$.18hb93fkpteuv$.dlg@40tude.net> In-Reply-To: <14p8llstxrtci$.18hb93fkpteuv$.dlg@40tude.net> Message-ID: <4ecd0652$0$6582$9b4e6d93@newsspool3.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 23 Nov 2011 15:42:26 CET NNTP-Posting-Host: 7725d2c8.newsspool3.arcor-online.net X-Trace: DXC=oYh@UlABXMU\9P[:DUn00QMcF=Q^Z^V3X4Fo<]lROoRQ8kFZLh>_cHTX3j];<>\L1a On 23.11.11 14:30, Dmitry A. Kazakov wrote: >>> So it is the debugging driven design you are advocating for. Designing by >>> fixing bugs. Nice, very nice... exactly the thing I don't want for Ada. >> >> Specifications have bugs. > > That is irrelevant to the discussion about designing programs. If you want > to switch to designing specifications then what do run-time assertions have > to do with that? Run-time assertions will tell when there probably is something wrong with any of: the specification; the program that should implement it; the compiler; the hardware; ... >>> One of the key points of good design is NOT to have such descriptions. The >>> reader of the program, be it human or the compiler should be able to >>> *understand* what you are describing. >> >> What is it that a reader of a package spec should be able to understand? > > The package specification, I suppose. > >> ADTs without invariants? > > Invariant is an implementation detail No, there is no implementation in a DbC contract. There is, however, a contractual obligation that each instance of a DbC type establish, at certain points, an invariant that its programmer has expressed in terms of publicly visible "features" of the type. (Ideally, these will be expressions involving idempotent functions). The actual properties of implementations are not relevant to the DbC client, only the properties expressed in the contract. >> Subprograms of unknown effect, > > You confuse interface and implementation. I call a subprogram because it has an effect. Is this unusual? In order to choose the right subprogram, I need to know its effect. There is very little that a subprogram profile tells about the body's effect. By comparison, an ADT that specifies preconditions, postconditions, and DbC-invariants, lets me know more about what will be the case after the body has executed successfully, or failed. >>>> There is no right or wrong in most programs. >>> >>> You cannot build safe software on false premises. >> >> Almost all programs have a number of things that can go wrong, > > Program code cannot GO wrong, it IS either wrong or not, here and now. No, we don't know whether an executable program is right or wrong, for almost all programs. We can detect that a run of a program has a certain effect. From the effects, we tend to conclude that a program has this or that property. But in general, this is just as wrong, we might see false positives, do not notice something that someone else will later notice, or be wrong about diagnosing right or wrong. But we have an issue, and look into it. If an executable program is not proven correct in all possible ways, we simply do not know what it is. We hope to have done our best, that's all. "Doctor, something hurts!" seems less useful than "Doctor, whenever I lift my left arm above the height of my shoulders, I could scream!".