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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,c9d5fc258548b22a X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!postnews.google.com!k15g2000prk.googlegroups.com!not-for-mail From: Shark8 Newsgroups: comp.lang.ada Subject: Re: How do I write directly to a memory address? Date: Wed, 9 Feb 2011 15:07:16 -0800 (PST) Organization: http://groups.google.com Message-ID: <159dca70-2103-46d7-beb2-c7754d30fe36@k15g2000prk.googlegroups.com> 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> NNTP-Posting-Host: 174.28.151.164 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1297292836 25410 127.0.0.1 (9 Feb 2011 23:07:16 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Wed, 9 Feb 2011 23:07:16 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: k15g2000prk.googlegroups.com; posting-host=174.28.151.164; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 6.0; en-US; rv:1.9.2.13) Gecko/20101203 Firefox/3.6.13 ( .NET CLR 3.5.30729; .NET4.0E),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:17188 Date: 2011-02-09T15:07:16-08:00 List-Id: On Feb 9, 3:31=A0pm, Hyman Rosen wrote: > On 2/9/2011 5:23 PM, Shark8 wrote: > > > > > On Feb 9, 3:09 pm, Hyman Rosen =A0wrote: > >> On 2/9/2011 4:40 PM, Shark8 wrote: > > >>> What induction *CAN* do is tell you whether or not SumTo > >>> is correctly constructed and that, barring exceptions, is > >>> what guarantees the return-value to be correct. > > >>> IE It is a proof of correctness; not per se a returner of values. > > >> Oh. OK, then. But I need to know what my SumTo function is going to > >> do with a given value of N. I'm trying to reason about the behavior > >> of my code here, not abstract math. > > > ...Ah, so then does this mean that when you're coding something up > > you don't care about "abstract logic"? > > > I hate to tell you {not really} but you JUST used "abstract math" when > > you presented a subprogram which yields the same results for any > > given input. IOW, you have shot your own argument down. > > Excuse me, but I really, truly do need to know what my > subprogram is going to do. People have been telling me > about "contracts" and "requirements" and "proofs of > correctness" and that Ada is good for stuff. So I have > this subprogram and I'd like to know what it will do > for different values of its parameter so I'll know if > I can use it or not. And you answered yourself when I asked you to prove your example would, in fact, return; that required you to justify usage of Random(). That you "need to know what it's doing" indicates to me one of two possibilities: either this function you have is not *really* yours but instead someone else's that you've 'inherited' OR you are attempting to use a tool {function/procedure} you do not fully understand for a problem you might not fully understand. Understanding a problem gives rise to the requirements and possibilities-of-solutions; this is what helps guide the 'contract' that *is* your subprogram's inputs and outputs. The 'tool' in this case could be a "containers"-object/package, or as it was in your example "Random()"... you were able to give an answer (to proving it returned) PRECISELY because you *knew* the details about that RNG. 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.