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!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx01.iad01.newshosting.com!newshosting.com!198.186.194.249.MISMATCH!transit3.readnews.com!news-out.readnews.com!postnews3.readnews.com!not-for-mail
Date: Wed, 09 Feb 2011 17:31:33 -0500
From: Hyman Rosen <hyrosen@mail.com>
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>
 <4d51905c$0$19486$882e7ee2@usenet-news.net>
 <36212a7b-deab-45d9-ac45-aa29cd90c7bc@o18g2000prh.googlegroups.com>
 <4d51a7bb$0$19486$882e7ee2@usenet-news.net> <iisll6$9th$1@munin.nbi.dk>
 <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>
 <e1076cab-2a7e-4762-acf4-80bf807614bf@n16g2000prc.googlegroups.com>
 <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>
In-Reply-To: 
 <9bff52ca-6213-41da-8fa4-3a4cdd8086d3@y36g2000pra.googlegroups.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <4d5315c8$0$18057$882e7ee2@usenet-news.net>
NNTP-Posting-Host: 0418c430.usenet-news.net
X-Trace: 
 DXC=bC\=Hh?75A?ZPi]J2cn8@?^oXGM_6\KV0mX0AG3X_jU?<^JMhOhjP4>VjKk:Lk^BN1cR12TN^Bg7>CKIHCW3N^V4OiaDcmXlf@5
X-Complaints-To: abuse@usenet-news.net
Xref: g2news1.google.com comp.lang.ada:17182
Date: 2011-02-09T17:31:33-05:00
List-Id: <comp.lang.ada>

On 2/9/2011 5:23 PM, Shark8 wrote:
> On Feb 9, 3:09 pm, Hyman Rosen<hyro...@mail.com>  wrote:
>> 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.