From: Mark Lorenzen <mark.lorenzen@gmail.com>
Subject: Re: SPARK : third example for Roesetta - reviewers welcome
Date: Mon, 16 Aug 2010 10:07:39 -0700 (PDT)
Date: 2010-08-16T10:07:39-07:00 [thread overview]
Message-ID: <eacd42c3-99ac-464b-a5be-450e24d7c934@f6g2000yqa.googlegroups.com> (raw)
In-Reply-To: op.vhjh1gnqxmjfy8@garhos
On 16 Aug., 18:42, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
ks
>
> In the real world now: I understand your point about what a SPARK program
> is really. But do you see a reason why SPARK should disallow defensive
> programming ? (forget about the suggestion to handle empty array in SPARK,
> 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
next prev parent reply other threads:[~2010-08-16 17:07 UTC|newest]
Thread overview: 61+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-08-15 6:17 SPARK : third example for Roesetta - reviewers welcome Yannick Duchêne (Hibou57)
2010-08-15 6:27 ` Yannick Duchêne (Hibou57)
2010-08-15 6:35 ` Jeffrey Carter
2010-08-15 6:39 ` Yannick Duchêne (Hibou57)
2010-08-15 18:42 ` Phil Thornley
2010-08-15 19:32 ` Yannick Duchêne (Hibou57)
2010-08-15 20:12 ` Phil Thornley
2010-08-16 10:08 ` Jacob Sparre Andersen
2010-08-15 19:57 ` Yannick Duchêne (Hibou57)
2010-08-15 20:07 ` Yannick Duchêne (Hibou57)
2010-08-15 20:57 ` Yannick Duchêne (Hibou57)
2010-08-15 22:19 ` Yannick Duchêne (Hibou57)
2010-08-16 5:51 ` Phil Thornley
2010-08-16 16:42 ` Yannick Duchêne (Hibou57)
2010-08-16 17:07 ` Mark Lorenzen [this message]
2010-08-15 22:09 ` Jeffrey Carter
2010-08-15 22:27 ` Yannick Duchêne (Hibou57)
2010-08-16 4:58 ` Phil Thornley
2010-08-16 7:50 ` Stephen Leake
2010-08-16 8:37 ` Phil Thornley
2010-08-16 16:55 ` Yannick Duchêne (Hibou57)
2010-08-16 20:40 ` Peter C. Chapin
2010-08-16 22:38 ` Yannick Duchêne (Hibou57)
2010-08-16 23:43 ` Peter C. Chapin
2010-08-17 9:15 ` Phil Thornley
2010-08-17 10:32 ` Peter C. Chapin
2010-08-17 19:53 ` Phil Thornley
2010-08-17 22:15 ` Dmitry A. Kazakov
2010-08-18 10:44 ` Phil Thornley
2010-08-18 16:33 ` Dmitry A. Kazakov
2010-08-19 6:19 ` Categories for SPARK on Rosetta Code (Was: SPARK : third example for Roesetta - reviewers welcome) Jacob Sparre Andersen
2010-08-20 8:40 ` Phil Thornley
2010-08-20 9:15 ` J-P. Rosen
2010-08-20 9:23 ` Dmitry A. Kazakov
2010-08-20 9:55 ` J-P. Rosen
2010-08-20 10:24 ` Dmitry A. Kazakov
2010-08-20 11:36 ` J-P. Rosen
2010-08-20 12:25 ` Dmitry A. Kazakov
2010-08-20 13:28 ` J-P. Rosen
2010-08-20 14:05 ` Dmitry A. Kazakov
2010-08-20 16:23 ` J-P. Rosen
2010-08-20 16:41 ` Dmitry A. Kazakov
2010-08-20 15:34 ` (see below)
2010-08-20 16:42 ` Dmitry A. Kazakov
2010-08-22 8:11 ` Categories for SPARK on Rosetta Code Jacob Sparre Andersen
2010-08-22 8:53 ` Dmitry A. Kazakov
2010-08-20 8:37 ` SPARK : third example for Roesetta - reviewers welcome Phil Thornley
2010-08-17 8:16 ` How to structure examples for Rosetta Code (Was: SPARK : third example for Roesetta - reviewers welcome) Jacob Sparre Andersen
2010-08-17 19:16 ` How to structure examples for Rosetta Code Simon Wright
2010-08-17 20:53 ` Peter C. Chapin
2010-08-17 21:24 ` Simon Wright
2010-08-17 2:07 ` SPARK : third example for Roesetta - reviewers welcome Stephen Leake
2010-08-16 4:41 ` Phil Thornley
2010-08-16 17:03 ` Yannick Duchêne (Hibou57)
2010-08-15 20:04 ` Jacob Sparre Andersen
2010-08-15 20:19 ` Yannick Duchêne (Hibou57)
2010-08-15 21:40 ` Jeffrey Carter
2010-08-15 22:13 ` Yannick Duchêne (Hibou57)
2010-08-16 4:29 ` Phil Thornley
2010-08-16 17:11 ` Phil Thornley
2010-08-20 9:06 ` Phil Thornley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox