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: 103376,6d79efdb8dde2c5a
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!postnews.google.com!f6g2000yqa.googlegroups.com!not-for-mail
From: Mark Lorenzen <mark.lorenzen@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK : third example for Roesetta - reviewers welcome
Date: Mon, 16 Aug 2010 10:07:39 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <eacd42c3-99ac-464b-a5be-450e24d7c934@f6g2000yqa.googlegroups.com>
References: <op.vhguffh3ule2fv@garhos>
 <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com>
 <op.vhhy5vycule2fv@garhos> <op.vhh2zekiule2fv@garhos>
 <b9add87d-ce8b-4db8-a0df-5157b610e3ff@y11g2000yqm.googlegroups.com>
 <op.vhjh1gnqxmjfy8@garhos>
NNTP-Posting-Host: 193.163.1.105
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1281978459 22378 127.0.0.1 (16 Aug 2010 17:07:39
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 16 Aug 2010 17:07:39 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: f6g2000yqa.googlegroups.com; posting-host=193.163.1.105;
 posting-account=Srm5lQoAAAAEMX9rv2ilEKR6FDPapmSq
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; da; rv:1.9.2.8)
 Gecko/20100722 Firefox/3.6.8,gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:13420
Date: 2010-08-16T10:07:39-07:00
List-Id: <comp.lang.ada>

On 16 Aug., 18:42, Yannick Duch=EAne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
ks
>
> In the real world now: I understand your point about what a SPARK program=
 =A0
> is really. But do you see a reason why SPARK should disallow defensive =
=A0
> programming ? (forget about the suggestion to handle empty array in SPARK=
, =A0
> this was silly, but defensive programming may not be)

Defensive programming can cause problems when trying to obtain 100%
test coverage. This is of course especially true, when the defensive
parts cover situations "that can never occur". How do you trigger
these situations? Using preconditions (or e.g. more restricted ranges)
as has already been suggested, can eliminate a surprising number of
cases where defensive programming would typically be used in non-SPARK
code.

- Mark L