comp.lang.ada
 help / color / mirror / Atom feed
From: Maciej Sobczak <see.my.homepage@gmail.com>
Subject: Re: Lost in translation (with SPARK user rules)
Date: Fri, 28 May 2010 02:39:12 -0700 (PDT)
Date: 2010-05-28T02:39:12-07:00	[thread overview]
Message-ID: <b377ab0d-7573-4172-80a7-5138d488ede4@40g2000vbr.googlegroups.com> (raw)
In-Reply-To: 4bfebb3f$0$27571$ba4acef3@reader.news.orange.fr

On 27 Maj, 20:34, Pascal Obry <pas...@obry.net> wrote:

> Just curious, why do you feel that you still need to write tests after
> having run successfully the SPARK proof checker?

Because the SPARK proof checker does not guarantee the lack of
infinite loops in the program?

--
Maciej Sobczak



  parent reply	other threads:[~2010-05-28  9:39 UTC|newest]

Thread overview: 46+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2010-05-26 10:09 Lost in translation (with SPARK user rules) Yannick Duchêne (Hibou57)
2010-05-26 10:38 ` Phil Thornley
2010-05-26 10:57   ` Yannick Duchêne (Hibou57)
2010-05-26 14:15     ` Pascal Obry
2010-05-26 14:28       ` Dmitry A. Kazakov
2010-05-26 19:28         ` Yannick Duchêne (Hibou57)
2010-05-26 20:14           ` Dmitry A. Kazakov
2010-05-26 21:14             ` Yannick Duchêne (Hibou57)
2010-05-26 21:15               ` Yannick Duchêne (Hibou57)
2010-05-26 22:01             ` Peter C. Chapin
2010-05-27 12:32               ` Mark Lorenzen
2010-05-27 18:34               ` Pascal Obry
2010-05-27 19:18                 ` Yannick Duchêne (Hibou57)
2010-05-28  9:39                 ` Maciej Sobczak [this message]
2010-05-28 11:57                 ` SPARK and testing. Was: " Peter C. Chapin
2010-05-28 12:59                   ` SPARK and testing Peter C. Chapin
2010-05-28 23:06                     ` Yannick Duchêne (Hibou57)
2010-05-26 19:16       ` Lost in translation (with SPARK user rules) Yannick Duchêne (Hibou57)
2010-05-26 19:32         ` Pascal Obry
2010-05-26 20:56           ` Yannick Duchêne (Hibou57)
2010-05-26 22:06           ` Peter C. Chapin
2010-05-27 18:39             ` Pascal Obry
2010-05-26 22:17         ` Peter C. Chapin
2010-05-27 10:11       ` Sockets package in SPARK (Was: Lost in translation (with SPARK user rules)) Jacob Sparre Andersen
2010-05-27 18:41         ` Pascal Obry
2010-05-27 19:20           ` Yannick Duchêne (Hibou57)
2010-05-28  7:43             ` Sockets package in SPARK Jacob Sparre Andersen
2010-05-27  8:13     ` Lost in translation (with SPARK user rules) Yannick Duchêne (Hibou57)
2010-05-27 10:55       ` Yannick Duchêne (Hibou57)
2010-05-27 11:32         ` Yannick Duchêne (Hibou57)
2010-05-27 11:41           ` Phil Thornley
2010-05-27 12:42             ` Yannick Duchêne (Hibou57)
2010-05-27 12:22         ` stefan-lucks
2010-05-27 11:37           ` Yannick Duchêne (Hibou57)
2010-05-27 11:57           ` Phil Thornley
2010-05-27 12:36             ` Yannick Duchêne (Hibou57)
2010-05-27 13:38               ` Phil Thornley
2010-06-03  2:44                 ` Yannick Duchêne (Hibou57)
2010-05-27 19:53 ` Warren
2010-05-29 23:03 ` Yannick Duchêne (Hibou57)
2010-05-30  6:55   ` Yannick Duchêne (Hibou57)
2010-05-30  9:30     ` Phil Thornley
2010-05-30  9:46       ` Yannick Duchêne (Hibou57)
2010-05-30  9:26   ` Phil Thornley
2010-05-30  9:57     ` Yannick Duchêne (Hibou57)
2010-06-01  5:42 ` Yannick Duchêne (Hibou57)
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox