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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,c9d5fc258548b22a X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news2.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!novia!news-out.readnews.com!postnews3.readnews.com!not-for-mail Date: Wed, 09 Feb 2011 18:24:26 -0500 From: Hyman Rosen User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.13) Gecko/20101207 Thunderbird/3.1.7 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: How do I write directly to a memory address? References: <67063a5b-f588-45ea-bf22-ca4ba0196ee6@l11g2000yqb.googlegroups.com> <4d51a7bb$0$19486$882e7ee2@usenet-news.net> <4d52b489$0$19486$882e7ee2@usenet-news.net> <9a8njlwvey1p.1a96yvvgdf6yu.dlg@40tude.net> <4d52c5e5$0$19486$882e7ee2@usenet-news.net> <720b7e8f-1ae2-4b3b-851e-12b08b3c99e0@r4g2000prm.googlegroups.com> <4d52dd97$0$18057$882e7ee2@usenet-news.net> <9a8f406d-05ca-4bf3-8487-918d4e0dd634@o18g2000prh.googlegroups.com> <4d52ee47$0$18057$882e7ee2@usenet-news.net> <4d5306a0$0$18057$882e7ee2@usenet-news.net> <76c123ab-7425-44d8-b26d-b2b41a9aa42b@o7g2000prn.googlegroups.com> <4d5310ab$0$18057$882e7ee2@usenet-news.net> <9bff52ca-6213-41da-8fa4-3a4cdd8086d3@y36g2000pra.googlegroups.com> <4d5315c8$0$18057$882e7ee2@usenet-news.net> <159dca70-2103-46d7-beb2-c7754d30fe36@k15g2000prk.googlegroups.com> In-Reply-To: <159dca70-2103-46d7-beb2-c7754d30fe36@k15g2000prk.googlegroups.com> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <4d53222d$0$18057$882e7ee2@usenet-news.net> NNTP-Posting-Host: cf5d8c0a.usenet-news.net X-Trace: DXC=EQ=7hG0\kAB0ej:PKomR0A^oXGM_6\KV@mX0AG3X_jUO<^JMhOhjP4NVjKk:Lk^BNAcR12TN^Bg7NCKIHCW3N^VDOiaDcmXlf@E X-Complaints-To: abuse@usenet-news.net Xref: g2news1.google.com comp.lang.ada:17190 Date: 2011-02-09T18:24:26-05:00 List-Id: On 2/9/2011 6:07 PM, Shark8 wrote: > In this context your "I really need to know what my subprogram > is going to do" seems very much like some college-kid whining > about how he "really needs to know what happens in book X," > while decrying people telling him "read the book." > > This is precisely to say that just as in reading the book the > answer to the question is answered, so to is your "I need to > know what happens" answered when a) contracts are made > and enforced AND b) proofs of completeness& correctness > are done. OK, I see that my attempts at being Socratic and oracular are failing. What I'm trying to demonstrate is that the chatter here about requirements and specifications and contracts fails to capture essential aspects of programs and even in Ada there's a good chance that you'll have to read the bodies to know what's going on. (Thanks for playing into that with the "read the book" example.) The problem with my SumTo subprogram is that it's liable to raise Storage_Error for a wide range of legal arguments. The problem with my Exponent subprogram is that its running time is enormous. Neither of these aspects can be made visible through Ada language facilities, and typical mathematical proofs of correctness won't show you this either. Just like C programmers, you Ada folks still find a way to get your work done, though.